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 ^^ ((A |^ n) ^^ A) by A2, 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