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

let A be Subset of (); :: 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 ;
consider l being Nat such that
A5: m <= l and
A6: a in A |^ l by ;
A7: l + k >= m by ;
a ^ b in A |^ (l + k) by ;
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 ; :: thesis: verum