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 )
A1: C = dom f by FUNCT_2:def 1;
assume A2: min (f,g) = EMF C ; :: thesis: f \ g = f
A3: 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 )
A4: (EMF C) . x = min ((f . x),(g . x)) by A2, FUZZY_1:5;

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

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

(min (f,(1_minus g))) . x = min ((f . x),((1_minus g) . x)) by FUZZY_1:5
.= (min ((1_minus g),(EMF C))) . x by A5, FUZZY_1:5
.= (EMF C) . x by FUZZY_1:18 ;
hence ( x in C implies (min (f,(1_minus g))) . x = f . x ) by A5; :: thesis: verum

end;

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

(min (f,(1_minus g))) . x = min ((f . x),((1_minus g) . x)) by FUZZY_1:5
.= min ((f . x),(1 - ((EMF C) . x))) by A6, FUZZY_1:def 5
.= min ((f . x),((1_minus (EMF C)) . x)) by FUZZY_1:def 5
.= min ((f . x),((UMF C) . x)) by FUZZY_1:40
.= (min (f,(UMF C))) . x by FUZZY_1:5 ;
hence ( x in C implies (min (f,(1_minus g))) . x = f . x ) by FUZZY_1:18; :: thesis: verum

end;

end;

end;

C = dom (min (f,(1_minus g))) by FUNCT_2:def 1;
hence f \ g = f by A1, A3, PARTFUN1:5; :: thesis: verum