defpred S₁[ set , set , set ] means for B being Subset of T st B = $2 holds
$3 = B ^i ;
A1: for n being Nat
for x being Subset of T ex y being Subset of T st S₁[n,x,y]

proof

let n be Nat; :: thesis: for x being Subset of T ex y being Subset of T st S₁[n,x,y]
let x be Subset of T; :: thesis: ex y being Subset of T st S₁[n,x,y]
reconsider C = x as Subset of T ;
for B being Subset of T st B = x holds
C ^i = B ^i ;
hence ex y being Subset of T st S₁[n,x,y] ; :: thesis: verum

end;

ex f being sequence of (bool the carrier of T) st
( f . 0 = A & ( for n being Nat holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A1);
hence ex b₁ being sequence of (bool the carrier of T) st
( ( for n being Nat
for B being Subset of T st B = b₁ . n holds
b₁ . (n + 1) = B ^i ) & b₁ . 0 = A ) ; :: thesis: verum