thus ||.(0. l1_Space).|| = 0 by Th9; :: according to NORMSP_0:def 6 :: thesis: ( l1_Space is discerning & l1_Space is RealNormSpace-like & l1_Space is vector-distributive & l1_Space is scalar-distributive & l1_Space is scalar-associative & l1_Space is scalar-unital & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable )
thus ( l1_Space is discerning & l1_Space is RealNormSpace-like & l1_Space is vector-distributive & l1_Space is scalar-distributive & l1_Space is scalar-associative & l1_Space is scalar-unital & l1_Space is Abelian & l1_Space is add-associative & l1_Space is right_zeroed & l1_Space is right_complementable ) by Lm2, Th9, NORMSP_0:def 5, NORMSP_1:def 1, RSSPACE:15; :: thesis: verum