let C be non empty set ; :: thesis: for f, g being Membership_Func of C st min f,g = EMF C holds
f \ g = f
let f, g be Membership_Func of C; :: thesis: ( min f,g = EMF C implies f \ g = f )
assume A1: min f,g = EMF C ; :: thesis: f \ g = f
min f,(1_minus g) = f

proof

A2: ( C = dom (min f,(1_minus g)) & C = dom f ) by FUNCT_2:def 1;
for x being Element of C st x in C holds
(min f,(1_minus g)) . x = f . x

proof

let x be Element of C; :: thesis: ( x in C implies (min f,(1_minus g)) . x = f . x )
A3: (EMF C) . x = min (f . x),(g . x) by A1, FUZZY_1:6;

per cases ( f . x = (EMF C) . x or g . x = (EMF C) . x ) by A3, XXREAL_0:15;

suppose A4: f . x = (EMF C) . x ; :: thesis: ( x in C implies (min f,(1_minus g)) . x = f . x )

(min f,(1_minus g)) . x = f . x

proof

(min f,(1_minus g)) . x = min (f . x),((1_minus g) . x) by FUZZY_1:6
.= (min (1_minus g),(EMF C)) . x by A4, FUZZY_1:6
.= (EMF C) . x by FUZZY_1:19 ;
hence (min f,(1_minus g)) . x = f . x by A4; :: thesis: verum

end;

hence ( x in C implies (min f,(1_minus g)) . x = f . x ) ; :: thesis: verum

end;

suppose A5: g . x = (EMF C) . x ; :: thesis: ( x in C implies (min f,(1_minus g)) . x = f . x )

(min f,(1_minus g)) . x = f . x

proof

(min f,(1_minus g)) . x = min (f . x),((1_minus g) . x) by FUZZY_1:6
.= min (f . x),(1 - ((EMF C) . x)) by A5, FUZZY_1:def 6
.= min (f . x),((1_minus (EMF C)) . x) by FUZZY_1:def 6
.= min (f . x),((UMF C) . x) by FUZZY_1:44
.= (min f,(UMF C)) . x by FUZZY_1:6 ;
hence (min f,(1_minus g)) . x = f . x by FUZZY_1:19; :: thesis: verum

end;

hence ( x in C implies (min f,(1_minus g)) . x = f . x ) ; :: thesis: verum

end;

end;

end;

hence min f,(1_minus g) = f by A2, PARTFUN1:34; :: thesis: verum

end;

hence f \ g = f ; :: thesis: verum