let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds
( max f,(min f,g) = f & min f,(max f,g) = f )
let f, g be Membership_Func of C; :: thesis: ( max f,(min f,g) = f & min f,(max f,g) = f )
A1: C = dom (min f,(max f,g)) by FUNCT_2:def 1;
A2: for x being Element of C st x in C holds
(max f,(min f,g)) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (max f,(min f,g)) . x = f . x )
(max f,(min f,g)) . x = max (f . x),((min f,g) . x) by Def5
.= max (f . x),(min (f . x),(g . x)) by Def4
.= f . x by XXREAL_0:36 ;
hence ( x in C implies (max f,(min f,g)) . x = f . x ) ; :: thesis: verum

end;

A3: for x being Element of C st x in C holds
(min f,(max f,g)) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (min f,(max f,g)) . x = f . x )
(min f,(max f,g)) . x = min (f . x),((max f,g) . x) by Def4
.= min (f . x),(max (f . x),(g . x)) by Def5
.= f . x by XXREAL_0:35 ;
hence ( x in C implies (min f,(max f,g)) . x = f . x ) ; :: thesis: verum

end;

( C = dom (max f,(min f,g)) & C = dom f ) by FUNCT_2:def 1;
hence ( max f,(min f,g) = f & min f,(max f,g) = f ) by A1, A2, A3, PARTFUN1:34; :: thesis: verum