set A = (dom f) \/ X;
let R, T be Relation of ((dom f) \/ X),(((dom f) \/ X) *); :: thesis: ( ( for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in R iff ( a in dom f & f . a = len b ) ) ) & ( for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in T iff ( a in dom f & f . a = len b ) ) ) implies R = T )
assume that
A2: for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in R iff ( a in dom f & f . a = len b ) ) and
A3: for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in T iff ( a in dom f & f . a = len b ) ) ; :: thesis: R = T
for x, y being object holds
( [x,y] in R iff [x,y] in T )

proof

let x, y be object ; :: thesis: ( [x,y] in R iff [x,y] in T )
thus ( [x,y] in R implies [x,y] in T ) :: thesis: ( [x,y] in T implies [x,y] in R )

proof

assume A4: [x,y] in R ; :: thesis: [x,y] in T
then reconsider x1 = x as Element of (dom f) \/ X by ZFMISC_1:87;
reconsider y1 = y as Element of ((dom f) \/ X) * by A4, ZFMISC_1:87;
[x1,y1] in R by A4;
then A5: x1 in dom f by A2;
f . x1 = len y1 by A2, A4;
hence [x,y] in T by A3, A5; :: thesis: verum

end;

assume A6: [x,y] in T ; :: thesis: [x,y] in R
then reconsider x1 = x as Element of (dom f) \/ X by ZFMISC_1:87;
reconsider y1 = y as Element of ((dom f) \/ X) * by A6, ZFMISC_1:87;
[x1,y1] in T by A6;
then A7: x1 in dom f by A3;
f . x1 = len y1 by A3, A6;
hence [x,y] in R by A2, A7; :: thesis: verum

end;

hence R = T by RELAT_1:def 2; :: thesis: verum