Suggestion: Meet for functions

In FUNCT_6:def 4 to omit problems with identification change meet f ==> Meet f

In PROB_1:def 5 and PROB_3:def 9 Intersection should be synonym for Meet

PROB_1:29 should be generalized

for N being non empty set, A1 being Function of N,X holds x in Meet A iff for n being Element of N holds x in A1.n

and semi-generalized variant of PROB_3:56

for N being non empty set st dom F1 c= N holds F1 <> {} implies (x in Intersection F1 iff (for k being Element of N st k in dom F1 holds x in F1.k));

may be added somewhere (FUNCT_6?)

-- GrzegorzBancerek - 04 Jan 2006

-- Main.FMEditor

Follow up