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

let x be object ; :: 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
A2: a1 in A * and
A3: a2 in A and
A4: x = a1 ^ a2 by FLANG_1:def 1;
consider n being Nat such that
A5: a1 in A |^ n by A2, FLANG_1:41;
A6: n + 1 >= 1 by NAT_1:11;
a2 in A |^ 1 by A3, FLANG_1:25;
then a1 ^ a2 in A |^ (n + 1) by A5, FLANG_1:40;
hence x in A |^.. 1 by A4, A6, Th2; :: thesis: verum

end;

now :: thesis: for x being object st x in A |^.. 1 holds
x in (A *) ^^ A

let x be object ; :: 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
A7: n >= 1 and
A8: x in A |^ n by Th2;
consider m being Nat such that
A9: m + 1 = n by A7, NAT_1:6;
A |^ (m + 1) c= (A *) ^^ A by FLANG_1:51;
hence x in (A *) ^^ A by A8, A9; :: thesis: verum

end;

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