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

A3: now :: thesis: for m being Nat st S₁[m] holds
S₁[m + 1]

let m be Nat; :: thesis: ( S₁[m] implies S₁[b₁ + 1] )
assume A4: S₁[m] ; :: thesis: S₁[b₁ + 1]

per cases ( m <= 0 or m > 0 ) ;

suppose m <= 0 ; :: thesis: S₁[b₁ + 1]

then m = 0 ;
hence S₁[m + 1] by A1, FLANG_1:25; :: thesis: verum

end;

suppose m > 0 ; :: thesis: S₁[b₁ + 1]

then (A |^ m) ^^ A c= (B |^.. k) ^^ (B |^.. k) by A1, A4, FLANG_1:17;
then A |^ (m + 1) c= (B |^.. k) ^^ (B |^.. k) by FLANG_1:23;
then A5: A |^ (m + 1) c= B |^.. (k + k) by Th18;
B |^.. (k + k) c= B |^.. k by Th5, NAT_1:11;
hence S₁[m + 1] by A5, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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