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

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

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;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

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

x in (A *) ^^ A

hence
(A *) ^^ A = A |^.. 1
by A1, TARSKI:2; :: thesis: verumx 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;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