let r be Real; :: thesis: for v being VECTOR of Linear_Space_of_RealSequences holds r * v = r (#) (seq_id v)
let v be VECTOR of Linear_Space_of_RealSequences; :: thesis: r * v = r (#) (seq_id v)
reconsider r1 = r as Element of REAL by XREAL_0:def 1;
reconsider v1 = v as Element of Funcs (NAT,REAL) ;
reconsider h = (RealFuncExtMult NAT) . (r1,v1) as Real_Sequence by FUNCT_2:66;
h = r (#) (seq_id v)

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: h . n = (r (#) (seq_id v)) . n
thus h . n = r * (v1 . n) by FUNCSDOM:4
.= (r (#) (seq_id v)) . n by VALUED_1:6 ; :: thesis: verum

end;

hence r * v = r (#) (seq_id v) ; :: thesis: verum