theorem Th2: :: LPSPACC1:2

for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for V1 being non empty Subset of V
for d1 being Element of V1
for A being BinOp of V1
for M being Function of [:COMPLEX,V1:],V1 st d1 = 0. V & A = the addF of V || V1 & M = the Mult of V | [:COMPLEX,V1:] holds
( CLSStruct(# V1,d1,A,M #) is Abelian & CLSStruct(# V1,d1,A,M #) is add-associative & CLSStruct(# V1,d1,A,M #) is right_zeroed & CLSStruct(# V1,d1,A,M #) is vector-distributive & CLSStruct(# V1,d1,A,M #) is scalar-distributive & CLSStruct(# V1,d1,A,M #) is scalar-associative & CLSStruct(# V1,d1,A,M #) is scalar-unital )