:: deftheorem defines RealVectSpace LOPBAN_1:def 4 :
for X being non empty set
for Y being RealLinearSpace holds RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);