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

hence f \ g = f by A1, A3, PARTFUN1:5; :: thesis: verum

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

C = dom (min (f,(1_minus g)))
by FUNCT_2:def 1;
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;

end;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;

end;

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;.= (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

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;.= 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

hence f \ g = f by A1, A3, PARTFUN1:5; :: thesis: verum