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

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

let n be Element of NAT ; :: thesis: ((seq ^\ k) ^\ m) . n = (seq ^\ (k + m)) . 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 ^\ (k + m)) . n by NAT_1:def 3 ; :: thesis: verum

end;

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