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:19; :: thesis: verum