let E be set ; :: thesis: for A, B being Subset of (E ^omega)
for n being Nat st A c= B * holds
A |^ n c= B *
let A, B be Subset of (E ^omega); :: thesis: for n being Nat st A c= B * holds
A |^ n c= B *
let n be Nat; :: thesis: ( A c= B * implies A |^ n c= B * )
defpred S₁[ Nat] means A |^ $1 c= B * ;
assume A1: A c= B * ; :: thesis: A |^ n c= B *

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 (A |^ n) ^^ A c= B * by A1, Th46;
hence S₁[n + 1] by Th23; :: thesis: verum

end;

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