theorem Th10: :: LOPBAN_1:10

for X being non empty set
for Y being RealLinearSpace holds RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace