let E be set ; :: thesis: for A being Subset of (E ^omega ) holds A + = A |^.. 1
let A be Subset of (E ^omega ); :: thesis: A + = A |^.. 1

A1: now

let x be set ; :: thesis: ( x in A |^.. 1 implies x in A + )
assume x in A |^.. 1 ; :: thesis: x in A +
then consider k being Nat such that
A2: ( 1 <= k & x in A |^ k ) by Th2;
thus x in A + by A2, Th48; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in A + implies x in A |^.. 1 )
assume x in A + ; :: thesis: x in A |^.. 1
then consider k being Nat such that
A3: ( 0 < k & x in A |^ k ) by Th48;
0 + 1 <= k by A3, NAT_1:13;
hence x in A |^.. 1 by A3, Th2; :: thesis: verum

end;

hence A + = A |^.. 1 by A1, TARSKI:2; :: thesis: verum