let f be Functional of V; :: thesis: ( f is additive implies f is 0-preserving )
assume A1: f is additive ; :: thesis: f is 0-preserving
f . (0. V) = f . ((0. V) + (0. V)) by RLVECT_1:def 4
.= (f . (0. V)) + (f . (0. V)) by A1 ;
hence f . (0. V) = 0. INT.Ring ; :: according to HAHNBAN1:def 9 :: thesis: verum