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

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