let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds
( max f,g = EMF C iff ( f = EMF C & g = EMF C ) )
let f, g be Membership_Func of C; :: thesis: ( max f,g = EMF C iff ( f = EMF C & g = EMF C ) )
thus ( max f,g = EMF C implies ( f = EMF C & g = EMF C ) ) :: thesis: ( f = EMF C & g = EMF C implies max f,g = EMF C )

proof

assume A1: max f,g = EMF C ; :: thesis: ( f = EMF C & g = EMF C )
thus f = EMF C :: thesis: g = EMF C

proof

A2: ( C = dom f & C = dom (EMF C) ) by FUNCT_2:def 1;
for x being Element of C st x in C holds
f . x = (EMF C) . x

proof

let x be Element of C; :: thesis: ( x in C implies f . x = (EMF C) . x )
A3: (EMF C) . x <= f . x by Th17;
max (f . x),(g . x) = (EMF C) . x by A1, Def5;
then f . x <= (EMF C) . x by XXREAL_0:25;
hence ( x in C implies f . x = (EMF C) . x ) by A3, XXREAL_0:1; :: thesis: verum

end;

hence f = EMF C by A2, PARTFUN1:34; :: thesis: verum

end;

thus g = EMF C :: thesis: verum

proof

A4: ( C = dom g & C = dom (EMF C) ) by FUNCT_2:def 1;
for x being Element of C st x in C holds
g . x = (EMF C) . x

proof

let x be Element of C; :: thesis: ( x in C implies g . x = (EMF C) . x )
A5: (EMF C) . x <= g . x by Th17;
max (f . x),(g . x) = (EMF C) . x by A1, Def5;
then g . x <= (EMF C) . x by XXREAL_0:25;
hence ( x in C implies g . x = (EMF C) . x ) by A5, XXREAL_0:1; :: thesis: verum

end;

hence g = EMF C by A4, PARTFUN1:34; :: thesis: verum

end;

end;

assume ( f = EMF C & g = EMF C ) ; :: thesis: max f,g = EMF C
hence max f,g = EMF C ; :: thesis: verum