let C be non empty set ; :: thesis: for f, g being Membership_Func of C st f \ g = EMF C holds
g c=
let f, g be Membership_Func of C; :: thesis: ( f \ g = EMF C implies g c= )
assume A1: f \ g = EMF C ; :: thesis: g c=
let c be Element of C; :: according to FUZZY_1:def 2 :: thesis: f . c <= g . c
A2: min ((f . c),((1_minus g) . c)) = (EMF C) . c by A1, FUZZY_1:5;

per cases ( f . c = (EMF C) . c or (1_minus g) . c = (EMF C) . c ) by A2, XXREAL_0:15;

suppose f . c = (EMF C) . c ; :: thesis: f . c <= g . c

hence f . c <= g . c by FUZZY_1:16; :: thesis: verum

end;

suppose A3: (1_minus g) . c = (EMF C) . c ; :: thesis: f . c <= g . c

g . c = (1_minus (1_minus g)) . c
.= 1 - ((1_minus g) . c) by FUZZY_1:def 5
.= (1_minus (EMF C)) . c by A3, FUZZY_1:def 5
.= (UMF C) . c by FUZZY_1:40 ;
hence f . c <= g . c by FUZZY_1:16; :: thesis: verum

end;

end;