RLSStruct(# the carrier of (graphNSP T), the ZeroF of (graphNSP T), the addF of (graphNSP T), the Mult of (graphNSP T) #) is RealLinearSpace by RSSPACE:11;
hence ( graphNSP T is Abelian & graphNSP T is add-associative & graphNSP T is right_zeroed & graphNSP T is right_complementable & graphNSP T is scalar-distributive & graphNSP T is vector-distributive & graphNSP T is scalar-associative & graphNSP T is scalar-unital ) by RSSPACE3:2; :: thesis: verum