let C1, C2 be non empty set ; :: thesis: for f being RMembership_Func of C1,C2
for c being set holds
( 0 <= f . c & f . c <= 1 )
let f be RMembership_Func of C1,C2; :: thesis: for c being set holds
( 0 <= f . c & f . c <= 1 )
let c be set ; :: thesis: ( 0 <= f . c & f . c <= 1 )

per cases ( c in [:C1,C2:] or not c in [:C1,C2:] ) ;

suppose c in [:C1,C2:] ; :: thesis: ( 0 <= f . c & f . c <= 1 )

then reconsider c = c as Element of [:C1,C2:] ;
A1: f . c <= (Umf (C1,C2)) . c by FUZZY_2:52;
(Zmf (C1,C2)) . c <= f . c by FUZZY_2:52;
hence ( 0 <= f . c & f . c <= 1 ) by A1, FUNCT_3:def 3; :: thesis: verum

end;

suppose A2: not c in [:C1,C2:] ; :: thesis: ( 0 <= f . c & f . c <= 1 )

dom f = [:C1,C2:] by FUNCT_2:def 1;
hence ( 0 <= f . c & f . c <= 1 ) by A2, FUNCT_1:def 2; :: thesis: verum

end;

end;