let X be RealUnitarySpace; :: thesis: for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
let seq be sequence of X; :: thesis: for k, m being Nat holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
let k, m be Nat; :: thesis: (seq ^\ k) ^\ m = (seq ^\ m) ^\ k

now :: thesis: for n being Element of NAT holds ((seq ^\ k) ^\ m) . n = ((seq ^\ m) ^\ k) . n

let n be Element of NAT ; :: thesis: ((seq ^\ k) ^\ m) . n = ((seq ^\ m) ^\ k) . n
thus ((seq ^\ k) ^\ m) . n = (seq ^\ k) . (n + m) by NAT_1:def 3
.= seq . ((n + m) + k) by NAT_1:def 3
.= seq . ((n + k) + m)
.= (seq ^\ m) . (n + k) by NAT_1:def 3
.= ((seq ^\ m) ^\ k) . n by NAT_1:def 3 ; :: thesis: verum

end;

hence (seq ^\ k) ^\ m = (seq ^\ m) ^\ k by FUNCT_2:63; :: thesis: verum