let F, G be RMembership_Func of C1,C3; :: thesis: ( ( 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))) ; :: thesis: 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:]; :: thesis: ( 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; :: thesis: 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; :: thesis: verum