:: deftheorem defines LC_RLSpace RLVECT_2:def 19 :
for V being RealLinearSpace holds LC_RLSpace V = RLSStruct(# (LinComb V),(@ (ZeroLC V)),(LCAdd V),(LCMult V) #);