( 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:] & the normF of V = the normF of V | the carrier of V )
;

hence ex b_{1} being RealNormSpace st

( the carrier of b_{1} c= the carrier of V & 0. b_{1} = 0. V & the addF of b_{1} = the addF of V || the carrier of b_{1} & the Mult of b_{1} = the Mult of V | [:REAL, the carrier of b_{1}:] & the normF of b_{1} = the normF of V | the carrier of b_{1} )
; :: thesis: verum

hence ex b

( the carrier of b