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

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

let x be object ; :: thesis: ( x in (A |^.. m) ^^ (A *) implies x in A |^.. m )
assume x in (A |^.. m) ^^ (A *) ; :: thesis: x in A |^.. m
then consider a, b being Element of E ^omega such that
A1: a in A |^.. m and
A2: b in A * and
A3: x = a ^ b by FLANG_1:def 1;
consider k being Nat such that
A4: b in A |^ k by A2, FLANG_1:41;
consider l being Nat such that
A5: m <= l and
A6: a in A |^ l by A1, Th2;
A7: l + k >= m by A5, NAT_1:12;
a ^ b in A |^ (l + k) by A4, A6, FLANG_1:40;
hence x in A |^.. m by A3, A7, Th2; :: thesis: verum

end;

then A8: (A |^.. m) ^^ (A *) c= A |^.. m ;
<%> E in A * by FLANG_1:48;
then A |^.. m c= (A |^.. m) ^^ (A *) by FLANG_1:16;
hence (A |^.. m) ^^ (A *) = A |^.. m by A8, XBOOLE_0:def 10; :: thesis: verum