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 3 :: 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 RELAT_1:def 4;
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 set 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 RELAT_1:def 4;
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 consider e being set such that
A6: [e,b] in R and
A7: e in {a} by RELAT_1:def 13;
thus [a,b] in R by A6, A7, TARSKI:def 1; :: thesis: verum