set F1 = dom T;
reconsider F2 = {} as Element of dom T by TREES_1:22;
defpred S₁[ Nat, Element of dom T, Element of dom T] means $3 in succ $2;

A1: now :: thesis: for n being Nat
for x being Element of dom T ex y being Element of dom T st S₁[n,x,y]

let n be Nat; :: thesis: for x being Element of dom T ex y being Element of dom T st S₁[n,x,y]
let x be Element of dom T; :: thesis: ex y being Element of dom T st S₁[n,x,y]
consider y being object such that
A2: y in succ x by XBOOLE_0:def 1;
reconsider y = y as Element of dom T by A2;
thus ex y being Element of dom T st S₁[n,x,y] by A2; :: thesis: verum

end;

consider f being sequence of (dom T) such that
A3: ( f . 0 = F2 & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
thus ex b₁ being sequence of (dom T) st
( b₁ . 0 = {} & ( for k being Nat holds b₁ . (k + 1) in succ (b₁ . k) ) ) by A3; :: thesis: verum