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

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:19
.= (A |^.. n) ^^ ((A |^ k,l) ^^ A) by FLANG_1:19
.= (A |^.. n) ^^ (A ^^ (A |^ k,l)) by FLANG_2:36
.= ((A |^.. n) ^^ A) ^^ (A |^ k,l) by FLANG_1:19
.= (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