let E be set ; :: thesis: for A, B being Subset of (E ^omega)

for n being Nat st A c= B + & n > 0 holds

A |^.. n c= B +

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

A |^.. n c= B +

let n be Nat; :: thesis: ( A c= B + & n > 0 implies A |^.. n c= B + )

assume that

A1: A c= B + and

A2: n > 0 ; :: thesis: A |^.. n c= B +

A c= B |^.. 1 by A1, Th50;

then A |^.. n c= B |^.. 1 by A2, Th29;

hence A |^.. n c= B + by Th50; :: thesis: verum

for n being Nat st A c= B + & n > 0 holds

A |^.. n c= B +

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

A |^.. n c= B +

let n be Nat; :: thesis: ( A c= B + & n > 0 implies A |^.. n c= B + )

assume that

A1: A c= B + and

A2: n > 0 ; :: thesis: A |^.. n c= B +

A c= B |^.. 1 by A1, Th50;

then A |^.. n c= B |^.. 1 by A2, Th29;

hence A |^.. n c= B + by Th50; :: thesis: verum