let V be non empty Abelian add-associative right_zeroed RealLinearSpace-like RLSStruct ; :: thesis: 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 RealLinearSpace-like )
let V1 be non empty add-closed multi-closed Subset of V; :: thesis: ( 0. V in V1 implies ( 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 RealLinearSpace-like ) )
assume 0. V in V1 ; :: thesis: ( 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 RealLinearSpace-like )
then ( In (0. V),V1 = 0. V & Mult_ V1 = the Mult of V | [:REAL ,V1:] ) by FUNCT_7:def 1;
hence ( 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 RealLinearSpace-like ) by RLSUB132; :: thesis: verum