theorem Th3: :: LPSPACC1:3

for V being non empty Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
for V1 being non empty add-closed multi-closed Subset of V st 0. V in V1 holds
( CLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is Abelian & CLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is add-associative & CLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is right_zeroed & CLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is vector-distributive & CLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-distributive & CLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-associative & CLSStruct(# V1,(In ((0. V),V1)),(add| (V1,V)),(Mult_ V1) #) is scalar-unital )