defpred S₁[ set , set , set ] means ex B, C being Subset of (E ^omega ) st
( C = $3 & B = $2 & C = B ^^ A );
A1: for i being Element of NAT
for x being Element of bool (E ^omega ) ex y being Element of bool (E ^omega ) st S₁[i,x,y]

proof

let i be Element of NAT ; :: thesis: for x being Element of bool (E ^omega ) ex y being Element of bool (E ^omega ) st S₁[i,x,y]
let x be Element of bool (E ^omega ); :: thesis: ex y being Element of bool (E ^omega ) st S₁[i,x,y]
take x ^^ A ; :: thesis: S₁[i,x,x ^^ A]
thus S₁[i,x,x ^^ A] ; :: thesis: verum

end;

consider f being Function of NAT ,(bool (E ^omega )) such that
A2: ( f . 0 = {(<%> E)} & ( for i being Element of NAT holds S₁[i,f . i,f . (i + 1)] ) ) from RECDEF_1:sch 2(A1);
consider C being Subset of (E ^omega ) such that
A3: C = f . n ;
take C ; :: thesis: ex concat being Function of NAT ,(bool (E ^omega )) st
( C = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )

now

let i be Nat; :: thesis: f . (i + 1) = (f . i) ^^ A
reconsider j = i as Element of NAT by ORDINAL1:def 13;
ex B, C being Subset of (E ^omega ) st
( C = f . (j + 1) & B = f . j & C = B ^^ A ) by A2;
hence f . (i + 1) = (f . i) ^^ A ; :: thesis: verum

end;

hence ex concat being Function of NAT ,(bool (E ^omega )) st
( C = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) by A2, A3; :: thesis: verum