theorem Th3: :: LPSPACE1:3

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