let z be Complex; :: thesis: for v being VECTOR of Linear_Space_of_ComplexSequences holds z * v = z (#) (seq_id v)
let v be VECTOR of Linear_Space_of_ComplexSequences; :: thesis: z * v = z (#) (seq_id v)
reconsider r1 = z as Element of COMPLEX by XCMPLX_0:def 2;
reconsider v1 = v as Element of Funcs (NAT,COMPLEX) ;
reconsider h = (ComplexFuncExtMult NAT) . (r1,v1) as Complex_Sequence by FUNCT_2:66;
h = z (#) (seq_id v)

proof

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

end;

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