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 :: thesis: for x being object st x in A + holds
x in A |^.. 1

let x be object ; :: 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
A2: 0 < k and
A3: x in A |^ k by Th48;
0 + 1 <= k by A2, NAT_1:13;
hence x in A |^.. 1 by A3, Th2; :: thesis: verum

end;

now :: thesis: for x being object st x in A |^.. 1 holds
x in A +

let x be object ; :: thesis: ( x in A |^.. 1 implies x in A + )
assume x in A |^.. 1 ; :: thesis: x in A +
then ex k being Nat st
( 1 <= k & x in A |^ k ) by Th2;
hence x in A + by Th48; :: thesis: verum

end;

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