let C be non empty set ; :: thesis: for f being Membership_Func of C holds f \+\ (EMF C) = f
let f be Membership_Func of C; :: thesis: f \+\ (EMF C) = f
thus f \+\ (EMF C) = max ((min (f,(UMF C))),(min ((1_minus f),(EMF C)))) by Th39
.= max (f,(min ((1_minus f),(EMF C)))) by Th17
.= max (f,(EMF C)) by Th17
.= f by Th17 ; :: thesis: verum