let E be set ; :: thesis: for A, B being Subset of ()
for k, n being Nat st A c= B |^.. k & n > 0 holds
A |^ n c= B |^.. k

let A, B be Subset of (); :: 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 m = 0 ;
hence S1[m + 1] by ; :: thesis: verum
end;
suppose m > 0 ; :: thesis: S1[b1 + 1]
then (A |^ m) ^^ A c= (B |^.. k) ^^ (B |^.. k) by ;
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 ;
hence S1[m + 1] by ; :: 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