( the addF of V = the addF of V || the carrier of V & the Mult of V = the Mult of V | [:REAL, the carrier of V:] ) by RELSET_1:19;
hence ex b₁ being RealLinearSpace st
( the carrier of b₁ c= the carrier of V & 0. b₁ = 0. V & the addF of b₁ = the addF of V || the carrier of b₁ & the Mult of b₁ = the Mult of V | [:REAL, the carrier of b₁:] ) ; :: thesis: verum