defpred S1[ set , set , set ] means ex B, C being Subset of (E ^omega) st
( C = $3 & B = $2 & C = B ^^ A );
A1: for i being Nat
for x being Element of bool (E ^omega) ex y being Element of bool (E ^omega) st S1[i,x,y]
proof
let i be Nat; :: thesis: for x being Element of bool (E ^omega) ex y being Element of bool (E ^omega) st S1[i,x,y]
let x be Element of bool (E ^omega); :: thesis: ex y being Element of bool (E ^omega) st S1[i,x,y]
take x ^^ A ; :: thesis: S1[i,x,x ^^ A]
thus S1[i,x,x ^^ A] ; :: thesis: verum
end;
consider f being sequence of (bool (E ^omega)) such that
A2: ( f . 0 = {(<%> E)} & ( for i being Nat holds S1[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 sequence of (bool (E ^omega)) st
( C = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) )
now :: thesis: for i being Nat holds f . (i + 1) = (f . i) ^^ A
let i be Nat; :: thesis: f . (i + 1) = (f . i) ^^ A
reconsider j = i as Element of NAT by ORDINAL1:def 12;
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 sequence of (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