let F, G be RMembership_Func of C1,C3; ( ( for x, z being object st [x,z] in [:C1,C3:] holds
F . (x,z) = upper_bound (rng (min (h,g,x,z))) ) & ( for x, z being object st [x,z] in [:C1,C3:] holds
G . (x,z) = upper_bound (rng (min (h,g,x,z))) ) implies F = G )
assume that
A21:
for x, z being object st [x,z] in [:C1,C3:] holds
F . (x,z) = upper_bound (rng (min (h,g,x,z)))
and
A22:
for x, z being object st [x,z] in [:C1,C3:] holds
G . (x,z) = upper_bound (rng (min (h,g,x,z)))
; F = G
A23:
for c being Element of [:C1,C3:] st c in [:C1,C3:] holds
F . c = G . c
proof
let c be
Element of
[:C1,C3:];
( c in [:C1,C3:] implies F . c = G . c )
consider x,
z being
object such that
x in C1
and
z in C3
and A24:
c = [x,z]
by ZFMISC_1:def 2;
reconsider z =
z,
x =
x as
set by TARSKI:1;
A25:
G . (
x,
z)
= upper_bound (rng (min (h,g,x,z)))
by A22, A24;
F . (
x,
z)
= upper_bound (rng (min (h,g,x,z)))
by A21, A24;
hence
(
c in [:C1,C3:] implies
F . c = G . c )
by A24, A25;
verum
end;
A26:
dom G = [:C1,C3:]
by FUNCT_2:def 1;
dom F = [:C1,C3:]
by FUNCT_2:def 1;
hence
F = G
by A26, A23, PARTFUN1:5; verum