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 )

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

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 A4:
[a,b] in S
; :: thesis: [a,b] in R
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;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

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