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 )

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

( 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
( f = EMF C & g = EMF C )
; :: thesis: max (f,g) = EMF C
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

g . x = (EMF C) . x

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;A2: for x being Element of C st x in C holds

f . x = (EMF C) . x

proof

A4:
for x being Element of C st x in C holds
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;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

g . x = (EMF C) . x

proof

( C = dom f & C = dom (EMF C) )
by FUNCT_2:def 1;
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;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

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

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