let N be set ; :: thesis: for R, S being Relation of N st ( for i being set st i in N holds
Im (R,i) = Im (S,i) ) holds
R = S
let R, S be Relation of N; :: thesis: ( ( for i being set st i in N holds
Im (R,i) = Im (S,i) ) implies R = S )
assume A1: for i being set st i in N holds
Im (R,i) = Im (S,i) ; :: thesis: R = S
let a, b be Element of N; :: according to RELSET_1:def 2 :: thesis: ( [a,b] in R iff [a,b] in S )
thus ( [a,b] in R implies [a,b] in S ) :: thesis: ( [a,b] in S implies [a,b] in R )

proof

assume A2: [a,b] in R ; :: thesis: [a,b] in S
then A3: a in dom R by XTUPLE_0:def 12;
a in {a} by TARSKI:def 1;
then b in Im (R,a) by A2, RELAT_1:def 13;
then b in Im (S,a) by A1, A3;
then ex e being object st
( [e,b] in S & e in {a} ) by RELAT_1:def 13;
hence [a,b] in S by TARSKI:def 1; :: thesis: verum

end;

assume A4: [a,b] in S ; :: thesis: [a,b] in R
then A5: a in dom S by XTUPLE_0:def 12;
a in {a} by TARSKI:def 1;
then b in Im (S,a) by A4, RELAT_1:def 13;
then b in Im (R,a) by A1, A5;
then ex e being object st
( [e,b] in R & e in {a} ) by RELAT_1:def 13;
hence [a,b] in R by TARSKI:def 1; :: thesis: verum