let C1, C2 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2 holds
( max (f,(Umf (C1,C2))) = Umf (C1,C2) & min (f,(Umf (C1,C2))) = f & max (f,(Zmf (C1,C2))) = f & min (f,(Zmf (C1,C2))) = Zmf (C1,C2) )
let f be RMembership_Func of C1,C2; :: thesis: ( max (f,(Umf (C1,C2))) = Umf (C1,C2) & min (f,(Umf (C1,C2))) = f & max (f,(Zmf (C1,C2))) = f & min (f,(Zmf (C1,C2))) = Zmf (C1,C2) )
A1: Umf (C1,C2) = UMF [:C1,C2:] ;
Zmf (C1,C2) = EMF [:C1,C2:] ;
hence ( max (f,(Umf (C1,C2))) = Umf (C1,C2) & min (f,(Umf (C1,C2))) = f & max (f,(Zmf (C1,C2))) = f & min (f,(Zmf (C1,C2))) = Zmf (C1,C2) ) by A1, FUZZY_1:18; :: thesis: verum