set l = R_NormSpace_of_ContinuousFunctions (S,T);
RLSStruct(# the carrier of (R_NormSpace_of_ContinuousFunctions (S,T)), the ZeroF of (R_NormSpace_of_ContinuousFunctions (S,T)), the addF of (R_NormSpace_of_ContinuousFunctions (S,T)), the Mult of (R_NormSpace_of_ContinuousFunctions (S,T)) #) = R_VectorSpace_of_ContinuousFunctions (S,T) ;
hence ( not R_NormSpace_of_ContinuousFunctions (S,T) is empty & R_NormSpace_of_ContinuousFunctions (S,T) is right_complementable & R_NormSpace_of_ContinuousFunctions (S,T) is Abelian & R_NormSpace_of_ContinuousFunctions (S,T) is add-associative & R_NormSpace_of_ContinuousFunctions (S,T) is right_zeroed & R_NormSpace_of_ContinuousFunctions (S,T) is vector-distributive & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-distributive & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-associative & R_NormSpace_of_ContinuousFunctions (S,T) is scalar-unital ) by RSSPACE3:2; :: thesis: verum