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 Th44
.= max f,(min (1_minus f),(EMF C)) by Th19
.= max f,(EMF C) by Th19
.= f by Th19 ; :: thesis: verum