for V being RealUnitarySpace
for V1 being Subset of V
for D being non empty set
for d1 being Element of D
for A being BinOp of D
for M being Function of [:REAL,D:],D
for S being Function of [:D,D:],REAL st V1 = D & d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:REAL,V1:] & S = the scalar of V || V1 holds
UNITSTR(# D,d1,A,M,S #) is Subspace of V