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 S1[ Nat] means ( $1 > 0 implies A |^ $1 c= B |^.. k );
A3: now :: thesis: for m being Nat st S1[m] holds
S1[m + 1]
let m be Nat; :: thesis: ( S1[m] implies S1[b1 + 1] )
assume A4: S1[m] ; :: thesis: S1[b1 + 1]
per cases ( m <= 0 or m > 0 ) ;
suppose m > 0 ; :: thesis: S1[b1 + 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 S1[m + 1] by A5, XBOOLE_1:1; :: thesis: verum
end;
end;
end;
A6: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch 2(A6, A3);
 hence A |^ n c= B |^.. k by A2; :: thesis: verum