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

for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)

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

let m be Nat; :: thesis: (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)

thus (A |^.. m) ^^ (A *) = (A |^.. m) ^^ (A |^.. 0) by Th11

.= (A |^.. 0) ^^ (A |^.. m) by Th27

.= (A *) ^^ (A |^.. m) by Th11 ; :: thesis: verum

for m being Nat holds (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)

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

let m be Nat; :: thesis: (A |^.. m) ^^ (A *) = (A *) ^^ (A |^.. m)

thus (A |^.. m) ^^ (A *) = (A |^.. m) ^^ (A |^.. 0) by Th11

.= (A |^.. 0) ^^ (A |^.. m) by Th27

.= (A *) ^^ (A |^.. m) by Th11 ; :: thesis: verum