let F, G be RMembership_Func of C1,C2; :: thesis: ( ( for x, y being object 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 object 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
A15: for x, y being object st [x,y] in [:C1,C2:] holds
( ( x = y implies F . (x,y) = 1 ) & ( x <> y implies F . (x,y) = 0 ) ) and
A16: for x, y being object st [x,y] in [:C1,C2:] holds
( ( x = y implies G . (x,y) = 1 ) & ( x <> y implies G . (x,y) = 0 ) ) ; :: thesis: F = G
A17: for x, y being object st x in C1 & y in C2 holds
F . (x,y) = G . (x,y)

proof

let x, y be object ; :: thesis: ( x in C1 & y in C2 implies F . (x,y) = G . (x,y) )
assume that
A18: x in C1 and
A19: y in C2 ; :: thesis: F . (x,y) = G . (x,y)
A20: [x,y] in [:C1,C2:] by A18, A19, ZFMISC_1:87;
then A21: ( not x = y implies F . (x,y) = 0 ) by A15;
( x = y implies F . (x,y) = 1 ) by A15, A20;
hence F . (x,y) = G . (x,y) by A16, A20, A21; :: thesis: verum

end;

thus F = G by A17; :: thesis: verum