theorem :: RSSPACE3:2

for l being NORMSTR st RLSStruct(# the carrier of l, the ZeroF of l, the addF of l, the Mult of l #) is RealLinearSpace holds
l is RealLinearSpace by RSSPACE:15;