let F, G be RMembership_Func of C1,C2; :: thesis: ( ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies F . x,y = 1 ) & ( x <> y implies F . x,y = 0 ) ) ) & ( for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies G . x,y = 1 ) & ( x <> y implies G . x,y = 0 ) ) ) implies F = G )
assume that
A9: for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies F . x,y = 1 ) & ( x <> y implies F . x,y = 0 ) ) and
A10: for x, y being set st [x,y] in [:C1,C2:] holds
( ( x = y implies G . x,y = 1 ) & ( x <> y implies G . x,y = 0 ) ) ; :: thesis: F = G
A11: ( dom F = [:C1,C2:] & dom G = [:C1,C2:] ) by FUNCT_2:def 1;
for x, y being set st x in C1 & y in C2 holds
F . x,y = G . x,y

proof

let x, y be set ; :: thesis: ( x in C1 & y in C2 implies F . x,y = G . x,y )
assume ( x in C1 & y in C2 ) ; :: thesis: F . x,y = G . x,y
then [x,y] in [:C1,C2:] by ZFMISC_1:106;
then ( ( x = y implies F . x,y = 1 ) & ( not x = y implies F . x,y = 0 ) & ( x = y implies G . x,y = 1 ) & ( not x = y implies G . x,y = 0 ) ) by A9, A10;
hence F . x,y = G . x,y ; :: thesis: verum

end;

hence F = G by A11, FUNCT_3:6; :: thesis: verum