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:6;

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:6
.= (min (1_minus g),(EMF C)) . x by A5, FUZZY_1:6
.= (EMF C) . x by FUZZY_1:19 ;
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:6
.= min (f . x),(1 - ((EMF C) . x)) by A6, 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 ( x in C implies (min f,(1_minus g)) . x = f . x ) by FUZZY_1:19; :: 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:34; :: thesis: verum