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