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 set holds
( [x,y] in R iff [x,y] in T )

proof

let x, y be set ; :: 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:106;
reconsider y1 = y as Element of ((dom f) \/ X) * by A4, ZFMISC_1:106;
[x1,y1] in R by A4;
then ( x1 in dom f & f . x1 = len y1 ) by A2;
hence [x,y] in T by A3; :: thesis: verum

end;

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

end;

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