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)

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

hence
r * v = r (#) (seq_id v)
; :: thesis: verum
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;thus h . n = r * (v1 . n) by FUNCSDOM:4

.= (r (#) (seq_id v)) . n by VALUED_1:6 ; :: thesis: verum