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