let E be set ; :: thesis: for A being Subset of ()
for k, l, n being Nat holds (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l))

let A be Subset of (); :: 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 S1[ Nat] means (A |^ (k,l)) ^^ (A |^.. \$1) = (A |^.. \$1) ^^ (A |^ (k,l));
A1: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
(A |^ (k,l)) ^^ (A |^.. (n + 1)) = (A |^ (k,l)) ^^ ((A |^.. n) ^^ A) by Th16
.= ((A |^.. n) ^^ (A |^ (k,l))) ^^ A by
.= (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 S1[n + 1] ; :: thesis: verum
end;
(A |^ (k,l)) ^^ () = (A |^ (k,l)) ^^ (A *) by Th11
.= (A *) ^^ (A |^ (k,l)) by FLANG_2:66
.= () ^^ (A |^ (k,l)) by Th11 ;
then A3: S1[ 0 ] ;
for n being Nat holds S1[n] from NAT_1:sch 2(A3, A1);
hence (A |^ (k,l)) ^^ (A |^.. n) = (A |^.. n) ^^ (A |^ (k,l)) ; :: thesis: verum