let E be set ; :: thesis:
let A be Subset of (E ^omega); :: thesis:

let x be object ; :: thesis:
assume x in (A *) ^^ A ; :: thesis:
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:

end;

let x be object ; :: thesis:
assume x in A |^.. 1 ; :: thesis:
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:

end;