let r be Real; :: thesis: for N, n being Nat
for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n)
let N, n be Nat; :: thesis: for seq being Real_Sequence of N holds (r * seq) . n = r * (seq . n)
let seq be Real_Sequence of N; :: thesis: (r * seq) . n = r * (seq . n)
reconsider m = n as Element of NAT by ORDINAL1:def 12;
A1: dom (r * seq) = NAT by FUNCT_2:def 1;
thus (r * seq) . n = (r * seq) /. m
.= r * (seq /. m) by A1, VFUNCT_1:def 4
.= r * (seq . n) ; :: thesis: verum