let C1, C2, C3 be non empty set ; for f being RMembership_Func of C2,C3 holds (Zmf (C1,C2)) (#) f = Zmf (C1,C3)
let f be RMembership_Func of C2,C3; (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:];
( 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 )
;
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; verum