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

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

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

then A8:
(A |^.. m) ^^ (A *) c= A |^.. m
;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;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

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