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_{1}[ Nat] means ( $1 > 0 implies A |^ $1 c= B |^.. k );

_{1}[ 0 ]
;

for m being Nat holds S_{1}[m]
from NAT_1:sch 2(A6, A3);

hence A |^ n c= B |^.. k by A2; :: thesis: verum

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

A3: now :: thesis: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]

A6:
SS

let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[b_{1} + 1] )

assume A4: S_{1}[m]
; :: thesis: S_{1}[b_{1} + 1]

end;assume A4: S

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

end;

suppose
m > 0
; :: thesis: S_{1}[b_{1} + 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_{1}[m + 1]
by A5, XBOOLE_1:1; :: thesis: verum

end;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

for m being Nat holds S

hence A |^ n c= B |^.. k by A2; :: thesis: verum