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 |^ n
let A, B be Subset of (E ^omega ); :: thesis: for n being Nat st A c= B holds
A |^ n c= B |^ n
let n be Nat; :: thesis: ( A c= B implies A |^ n c= B |^ n )
assume A1: A c= B ; :: thesis: A |^ n c= B |^ n
defpred S₁[ Nat] means A |^ $1 c= B |^ $1;
A2: S₁[ 0 ]

proof

( A |^ 0 = {(<%> E)} & B |^ 0 = {(<%> E)} ) by Th25;
hence S₁[ 0 ] ; :: thesis: verum

end;

A3: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
( (A |^ n) ^^ A = A |^ (n + 1) & (B |^ n) ^^ B = B |^ (n + 1) ) by Th24;
hence S₁[n + 1] by A1, A4, Th18; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence A |^ n c= B |^ n ; :: thesis: verum