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:30, CSSPACE:15, CSSPACE:def 20;
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:91, ZFMISC_1:119;
u + v = (the addF of Linear_Space_of_ComplexSequences || the_set_of_l2ComplexSequences ) . [u,v] by CSSPACE:14, CSSPACE:def 8, CSSPACE:def 20
.= u1 + v1 by A1, CSSPACE:def 20, FUNCT_1:70 ;
hence u + v = (seq_id u) + (seq_id v) by CSSPACE:17; :: thesis: verum