set A = (dom f) \/ X;
defpred S₁[ Element of (dom f) \/ X, Element of ((dom f) \/ X) * ] means ( $1 in dom f & f . $1 = len $2 );
consider R being Relation of ((dom f) \/ X),(((dom f) \/ X) *) such that
A1: for x being Element of (dom f) \/ X
for y being Element of ((dom f) \/ X) * holds
( [x,y] in R iff S₁[x,y] ) from RELSET_1:sch 2();
take R ; :: 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 ) )
let a be Element of (dom f) \/ X; :: thesis: for b being Element of ((dom f) \/ X) * holds
( [a,b] in R iff ( a in dom f & f . a = len b ) )
let b be Element of ((dom f) \/ X) * ; :: thesis: ( [a,b] in R iff ( a in dom f & f . a = len b ) )
thus ( [a,b] in R iff ( a in dom f & f . a = len b ) ) by A1; :: thesis: verum