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

proof

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

end;

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

proof

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

end;

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