set W = the_set_of_l2ComplexSequences ;
set L1 = Linear_Space_of_ComplexSequences ;
let r be Complex; :: thesis: for u being VECTOR of Complex_l2_Space holds r * u = r (#) (seq_id u)
let u be VECTOR of Complex_l2_Space; :: thesis: r * u = r (#) (seq_id u)
reconsider u1 = u as VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1:29, CSSPACE:13;
dom the Mult of Linear_Space_of_ComplexSequences = [:COMPLEX, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def 1;
then A1: dom ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l2ComplexSequences:]) = [:COMPLEX,the_set_of_l2ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
reconsider r = r as Element of COMPLEX by XCMPLX_0:def 2;
r * u = the Mult of Complex_l2_Space . [r,u] by CLVECT_1:def 1
.= ( the Mult of Linear_Space_of_ComplexSequences | [:COMPLEX,the_set_of_l2ComplexSequences:]) . [r,u] by CSSPACE:def 9
.= the Mult of Linear_Space_of_ComplexSequences . [r,u] by A1, FUNCT_1:47
.= r * u1 by CLVECT_1:def 1 ;
hence r * u = r (#) (seq_id u) by CSSPACE:15; :: thesis: verum