let N be set ; 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; ( ( 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)
; R = S
let a, b be Element of N; RELSET_1:def 2 ( [a,b] in R iff [a,b] in S )
thus
( [a,b] in R implies [a,b] in S )
( [a,b] in S implies [a,b] in R )
assume A4:
[a,b] in S
; [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; verum