let C1, C2 be non empty set ; :: thesis: for f, g being RMembership_Func of C1,C2 st f \ g = Zmf (C1,C2) holds
g c=
let f, g be RMembership_Func of C1,C2; :: thesis: ( f \ g = Zmf (C1,C2) implies g c= )
Zmf (C1,C2) = EMF [:C1,C2:] ;
hence ( f \ g = Zmf (C1,C2) implies g c= ) by Th26; :: thesis: verum