thus 0. Complex_l2_Space = 0. Linear_Space_of_ComplexSequences by CSSPACE:def 10
.= CZeroseq ; :: thesis: verum