let N be Nat; :: thesis: for seq being Real_Sequence of N holds 1 * seq = seq
let seq be Real_Sequence of N; :: thesis: 1 * seq = seq
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (1 * seq) . n = seq . n
thus (1 * seq) . n = 1 * (seq . n) by Th5
.= seq . n by RLVECT_1:def 8 ; :: thesis: verum