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

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 |^ (k,l)) ^^ (A |^.. (n + 1)) = (A |^ (k,l)) ^^ ((A |^.. n) ^^ A) by Th16
.= ((A |^.. n) ^^ (A |^ (k,l))) ^^ A by A2, FLANG_1:18
.= (A |^.. n) ^^ ((A |^ (k,l)) ^^ A) by FLANG_1:18
.= (A |^.. n) ^^ (A ^^ (A |^ (k,l))) by FLANG_2:36
.= ((A |^.. n) ^^ A) ^^ (A |^ (k,l)) by FLANG_1:18
.= (A |^.. (n + 1)) ^^ (A |^ (k,l)) by Th16 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(A |^ (k,l)) ^^ (A |^.. 0) = (A |^ (k,l)) ^^ (A *) by Th11
.= (A *) ^^ (A |^ (k,l)) by FLANG_2:66
.= (A |^.. 0) ^^ (A |^ (k,l)) by Th11 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l)) ; :: thesis: verum