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