let C be non empty set ; :: thesis: for f being Membership_Func of C holds

( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

let f be Membership_Func of C; :: thesis: ( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

A1: ( C = dom (max (f,(EMF C))) & C = dom (min (f,(EMF C))) ) by FUNCT_2:def 1;

A2: for x being Element of C st x in C holds

(min (f,(UMF C))) . x = f . x

(min (f,(EMF C))) . x = (EMF C) . x

(max (f,(EMF C))) . x = f . x

hence max (f,(UMF C)) = UMF C by Lm1; :: thesis: ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

A8: C = dom (EMF C) by FUNCT_2:def 1;

( C = dom (min (f,(UMF C))) & C = dom f ) by FUNCT_2:def 1;

hence ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) by A2, A6, A1, A8, A4, PARTFUN1:5; :: thesis: verum

( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

let f be Membership_Func of C; :: thesis: ( max (f,(UMF C)) = UMF C & min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

A1: ( C = dom (max (f,(EMF C))) & C = dom (min (f,(EMF C))) ) by FUNCT_2:def 1;

A2: for x being Element of C st x in C holds

(min (f,(UMF C))) . x = f . 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 (min (f,(UMF C))) . x = f . x )

A3: f . x <= (UMF C) . x by Th15;

(min (f,(UMF C))) . x = min ((f . x),((UMF C) . x)) by Def3

.= f . x by A3, XXREAL_0:def 9 ;

hence ( x in C implies (min (f,(UMF C))) . x = f . x ) ; :: thesis: verum

end;A3: f . x <= (UMF C) . x by Th15;

(min (f,(UMF C))) . x = min ((f . x),((UMF C) . x)) by Def3

.= f . x by A3, XXREAL_0:def 9 ;

hence ( x in C implies (min (f,(UMF C))) . x = f . x ) ; :: thesis: verum

(min (f,(EMF C))) . x = (EMF C) . x

proof

A6:
for x being Element of C st x in C holds
let x be Element of C; :: thesis: ( x in C implies (min (f,(EMF C))) . x = (EMF C) . x )

A5: (EMF C) . x <= f . x by Th15;

(min (f,(EMF C))) . x = min ((f . x),((EMF C) . x)) by Def3

.= (EMF C) . x by A5, XXREAL_0:def 9 ;

hence ( x in C implies (min (f,(EMF C))) . x = (EMF C) . x ) ; :: thesis: verum

end;A5: (EMF C) . x <= f . x by Th15;

(min (f,(EMF C))) . x = min ((f . x),((EMF C) . x)) by Def3

.= (EMF C) . x by A5, XXREAL_0:def 9 ;

hence ( x in C implies (min (f,(EMF C))) . x = (EMF C) . x ) ; :: thesis: verum

(max (f,(EMF C))) . x = f . x

proof

( UMF C c= & max (f,(UMF C)) c= )
by Th14, Th16;
let x be Element of C; :: thesis: ( x in C implies (max (f,(EMF C))) . x = f . x )

A7: (EMF C) . x <= f . x by Th15;

(max (f,(EMF C))) . x = max ((f . x),((EMF C) . x)) by Def4

.= f . x by A7, XXREAL_0:def 10 ;

hence ( x in C implies (max (f,(EMF C))) . x = f . x ) ; :: thesis: verum

end;A7: (EMF C) . x <= f . x by Th15;

(max (f,(EMF C))) . x = max ((f . x),((EMF C) . x)) by Def4

.= f . x by A7, XXREAL_0:def 10 ;

hence ( x in C implies (max (f,(EMF C))) . x = f . x ) ; :: thesis: verum

hence max (f,(UMF C)) = UMF C by Lm1; :: thesis: ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C )

A8: C = dom (EMF C) by FUNCT_2:def 1;

( C = dom (min (f,(UMF C))) & C = dom f ) by FUNCT_2:def 1;

hence ( min (f,(UMF C)) = f & max (f,(EMF C)) = f & min (f,(EMF C)) = EMF C ) by A2, A6, A1, A8, A4, PARTFUN1:5; :: thesis: verum