thus 0. Complex_l2_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:12, CSSPACE:def 10, CSSPACE:def 18
.= CZeroseq by CSSPACE:def 7 ; :: thesis: verum