set V1 = a * V;
set Z0 = Zero_ (a,V);
set AV1 = Add_ (a,V);
set MV1 = Mult_ (a,V);
( Zero_ (a,V) = 0. V & Add_ (a,V) = the addF of V || (a * V) & Mult_ (a,V) = the lmult of V | [: the carrier of R,(a * V):] )
;
hence
ModuleStr(# (a * V),(Add_ (a,V)),(Zero_ (a,V)),(Mult_ (a,V)) #) is Subspace of V
by ZMODUL01:40; verum