let C2, C3, C1 be non empty set ; :: thesis: for f being RMembership_Func of C2,C3 holds (Zmf C1,C2) (#) f = Zmf C1,C3
let f be RMembership_Func of C2,C3; :: thesis: (Zmf C1,C2) (#) f = Zmf C1,C3
A1: ( dom ((Zmf C1,C2) (#) f) = [:C1,C3:] & dom (Zmf C1,C3) = [:C1,C3:] ) by FUNCT_2:def 1;
for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
((Zmf C1,C2) (#) f) . c = (Zmf C1,C3) . c

proof

let c be Element of [:C1,C3:]; :: thesis: ( c in [:C1,C3:] implies ((Zmf C1,C2) (#) f) . c = (Zmf C1,C3) . c )
consider x, z being set such that
A2: ( x in C1 & z in C3 & c = [x,z] ) by ZFMISC_1:def 2;
((Zmf C1,C2) (#) f) . c = ((Zmf C1,C2) (#) f) . x,z by A2
.= sup (rng (min (Zmf C1,C2),f,x,z)) by A2, Def3
.= (Zmf C1,C3) . c by A2, Lm6 ;
hence ( c in [:C1,C3:] implies ((Zmf C1,C2) (#) f) . c = (Zmf C1,C3) . c ) ; :: thesis: verum

end;

hence (Zmf C1,C2) (#) f = Zmf C1,C3 by A1, PARTFUN1:34; :: thesis: verum