let r be Real; :: thesis:
let v be VECTOR of Linear_Space_of_RealSequences; :: thesis:
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)

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

end;