thus Complex_l1_Space is reflexive :: thesis: ( Complex_l1_Space is discerning & Complex_l1_Space is ComplexNormSpace-like & Complex_l1_Space is vector-distributive & Complex_l1_Space is scalar-distributive & Complex_l1_Space is scalar-associative & Complex_l1_Space is scalar-unital & Complex_l1_Space is Abelian & Complex_l1_Space is add-associative & Complex_l1_Space is right_zeroed & Complex_l1_Space is right_complementable )

proof

thus ||.(0. Complex_l1_Space).|| = 0 by Th9; :: according to NORMSP_0:def 6 :: thesis: verum

end;

thus ( Complex_l1_Space is discerning & Complex_l1_Space is ComplexNormSpace-like & Complex_l1_Space is vector-distributive & Complex_l1_Space is scalar-distributive & Complex_l1_Space is scalar-associative & Complex_l1_Space is scalar-unital & Complex_l1_Space is Abelian & Complex_l1_Space is add-associative & Complex_l1_Space is right_zeroed & Complex_l1_Space is right_complementable ) by Lm3, Th9, CLVECT_1:def 13, CSSPACE:79, NORMSP_0:def 5; :: thesis: verum