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:] ;
( (Zmf C1,C2) . c <= f . c & f . c <= (Umf C1,C2) . c ) by FUZZY_2:57;
hence ( 0 <= f . c & f . c <= 1 ) by FUNCT_3:def 3; :: thesis: verum

end;

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

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

end;

end;