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

proof

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

end;

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