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:30, CSSPACE:15, CSSPACE:def 20;
set L1 = Linear_Space_of_ComplexSequences ;
set W = the_set_of_l2ComplexSequences ;
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:91, ZFMISC_1:119;
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:14, CSSPACE:def 9, CSSPACE:def 20
.= the Mult of Linear_Space_of_ComplexSequences . [r,u] by A1, CSSPACE:def 20, FUNCT_1:70
.= r * u1 by CLVECT_1:def 1 ;
hence r * u = r (#) (seq_id u) by CSSPACE:17; :: thesis: verum