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 Th31; :: thesis: verum