set W = the_set_of_l2ComplexSequences ;
set L1 = Linear_Space_of_ComplexSequences ;
let u, v be VECTOR of Complex_l2_Space; :: thesis: u + v = (seq_id u) + (seq_id v)
reconsider u1 = u, v1 = v as VECTOR of Linear_Space_of_ComplexSequences by CLVECT_1:29, CSSPACE:13;
dom the addF of Linear_Space_of_ComplexSequences = [: the carrier of Linear_Space_of_ComplexSequences, the carrier of Linear_Space_of_ComplexSequences:] by FUNCT_2:def 1;
then A1: dom ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences) = [:the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences:] by RELAT_1:62, ZFMISC_1:96;
u + v = ( the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences) . [u,v] by CSSPACE:def 8
.= u1 + v1 by A1, FUNCT_1:47 ;
hence u + v = (seq_id u) + (seq_id v) by CSSPACE:15; :: thesis: verum