let C1, C2, C3 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,C3)) = [:C1,C3:] by FUNCT_2:def 1;
A2: 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 object such that
A3: x in C1 and
A4: z in C3 and
A5: c = [x,z] by ZFMISC_1:def 2;
reconsider z = z, x = x as set by TARSKI:1;
((Zmf (C1,C2)) (#) f) . c = ((Zmf (C1,C2)) (#) f) . (x,z) by A5
.= upper_bound (rng (min ((Zmf (C1,C2)),f,x,z))) by A5, Def3
.= (Zmf (C1,C3)) . c by A3, A4, A5, Lm7 ;
hence ( c in [:C1,C3:] implies ((Zmf (C1,C2)) (#) f) . c = (Zmf (C1,C3)) . c ) ; :: thesis: verum

end;

dom ((Zmf (C1,C2)) (#) f) = [:C1,C3:] by FUNCT_2:def 1;
hence (Zmf (C1,C2)) (#) f = Zmf (C1,C3) by A1, A2, PARTFUN1:5; :: thesis: verum