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

A1: now

let x be set ; :: thesis: ( x in A |^.. 1 implies x in (A * ) ^^ A )
assume x in A |^.. 1 ; :: thesis: x in (A * ) ^^ A
then consider n being Nat such that
A2: ( n >= 1 & x in A |^ n ) by Th2;
consider m being Nat such that
A3: m + 1 = n by A2, NAT_1:6;
A |^ (m + 1) c= (A * ) ^^ A by FLANG_1:52;
hence x in (A * ) ^^ A by A2, A3; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in (A * ) ^^ A implies x in A |^.. 1 )
assume x in (A * ) ^^ A ; :: thesis: x in A |^.. 1
then consider a1, a2 being Element of E ^omega such that
A4: ( a1 in A * & a2 in A & x = a1 ^ a2 ) by FLANG_1:def 1;
A5: a2 in A |^ 1 by A4, FLANG_1:26;
consider n being Nat such that
A6: a1 in A |^ n by A4, FLANG_1:42;
( a1 ^ a2 in A |^ (n + 1) & n + 1 >= 1 ) by A5, A6, FLANG_1:41, NAT_1:11;
hence x in A |^.. 1 by A4, Th2; :: thesis: verum

end;

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