set T = NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #);
reconsider T = NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #) as non empty NORMSTR ;
then A1:
T is Abelian
;
then A2:
T is add-associative
;
then A3:
T is right_zeroed
;
A4:
T is right_complementable
then A5:
T is scalar-distributive
;
then A6:
T is vector-distributive
;
then A7:
T is scalar-associative
;
then A8:
T is scalar-unital
;
A9:
T is reflexive
by EUCLID:def 2, COMPLEX1:44;
then A10:
T is discerning
;
then
T is RealNormSpace-like
;
hence
NORMSTR(# REAL,(In (0,REAL)),addreal,multreal,absreal #) is RealNormSpace
by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10; verum