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