let E be set ; :: thesis: for A being Subset of (E ^omega )
for n being Nat holds (A |^ n) ^^ (A * ) = (A * ) ^^ (A |^ n)
let A be Subset of (E ^omega ); :: thesis: for n being Nat holds (A |^ n) ^^ (A * ) = (A * ) ^^ (A |^ n)
let n be Nat; :: thesis: (A |^ n) ^^ (A * ) = (A * ) ^^ (A |^ n)
defpred S₁[ Nat] means (A |^ $1) ^^ (A * ) = (A * ) ^^ (A |^ $1);

A1: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
(A |^ (n + 1)) ^^ (A * ) = ((A |^ n) ^^ A) ^^ (A * ) by Th24
.= (A |^ n) ^^ (A ^^ (A * )) by Th19
.= (A |^ n) ^^ ((A * ) ^^ A) by Th58
.= ((A * ) ^^ (A |^ n)) ^^ A by A2, Th19
.= (A * ) ^^ ((A |^ n) ^^ A) by Th19
.= (A * ) ^^ (A |^ (n + 1)) by Th24 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(A |^ 0 ) ^^ (A * ) = {(<%> E)} ^^ (A * ) by Th25
.= A * by Th14
.= (A * ) ^^ {(<%> E)} by Th14
.= (A * ) ^^ (A |^ 0 ) by Th25 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence (A |^ n) ^^ (A * ) = (A * ) ^^ (A |^ n) ; :: thesis: verum