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 :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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 Th23
.= (A |^ n) ^^ (A ^^ (A *)) by Th18
.= (A |^ n) ^^ ((A *) ^^ A) by Th57
.= ((A *) ^^ (A |^ n)) ^^ A by A2, Th18
.= (A *) ^^ ((A |^ n) ^^ A) by Th18
.= (A *) ^^ (A |^ (n + 1)) by Th23 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(A |^ 0) ^^ (A *) = {(<%> E)} ^^ (A *) by Th24
.= A * by Th13
.= (A *) ^^ {(<%> E)} by Th13
.= (A *) ^^ (A |^ 0) by Th24 ;
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