let F, G be RMembership_Func of C1,C3; :: thesis: ( ( for x, z being set st [x,z] in [:C1,C3:] holds
F . x,z = sup (rng (min h,g,x,z)) ) & ( for x, z being set st [x,z] in [:C1,C3:] holds
G . x,z = sup (rng (min h,g,x,z)) ) implies F = G )
assume that
A15: for x, z being set st [x,z] in [:C1,C3:] holds
F . x,z = sup (rng (min h,g,x,z)) and
A16: for x, z being set st [x,z] in [:C1,C3:] holds
G . x,z = sup (rng (min h,g,x,z)) ; :: thesis: F = G
A17: ( dom F = [:C1,C3:] & dom G = [:C1,C3:] ) by FUNCT_2:def 1;
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 set such that
A18: ( x in C1 & z in C3 & c = [x,z] ) by ZFMISC_1:def 2;
( F . x,z = sup (rng (min h,g,x,z)) & G . x,z = sup (rng (min h,g,x,z)) ) by A15, A16, A18;
hence ( c in [:C1,C3:] implies F . c = G . c ) by A18; :: thesis: verum

end;

hence F = G by A17, PARTFUN1:34; :: thesis: verum