let E be set ; :: thesis: for A being Subset of (E ^omega)
for n being Nat st <%> E in A holds
<%> E in A |^ n
let A be Subset of (E ^omega); :: thesis: for n being Nat st <%> E in A holds
<%> E in A |^ n
let n be Nat; :: thesis: ( <%> E in A implies <%> E in A |^ n )
defpred S₁[ Nat] means <%> E in A |^ $1;
assume A1: <%> E in A ; :: thesis: <%> E in A |^ n

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then <%> E in (A |^ n) ^^ A by A1, Th15;
hence S₁[n + 1] by Th23; :: thesis: verum

end;

A |^ 0 = {(<%> E)} by Th24;
then A3: S₁[ 0 ] by TARSKI:def 1;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2);
hence <%> E in A |^ n ; :: thesis: verum