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