theorem :: LOPBAN_1:13

for X being non empty set
for Y being RealLinearSpace holds 0. (RealVectSpace (X,Y)) = X --> (0. Y) ;