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 )
A2: 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 )
max ((f . x),(g . x)) = (EMF C) . x by A1, Def4;
then A3: f . x <= (EMF C) . x by XXREAL_0:25;
(EMF C) . x <= f . x by Th15;
hence ( x in C implies f . x = (EMF C) . x ) by A3, XXREAL_0:1; :: thesis: verum

end;

A4: 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 )
max ((f . x),(g . x)) = (EMF C) . x by A1, Def4;
then A5: g . x <= (EMF C) . x by XXREAL_0:25;
(EMF C) . x <= g . x by Th15;
hence ( x in C implies g . x = (EMF C) . x ) by A5, XXREAL_0:1; :: thesis: verum

end;

( C = dom f & C = dom (EMF C) ) by FUNCT_2:def 1;
hence f = EMF C by A2, PARTFUN1:5; :: thesis: g = EMF C
( C = dom g & C = dom (EMF C) ) by FUNCT_2:def 1;
hence g = EMF C by A4, PARTFUN1:5; :: thesis: verum

end;

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