let V be RealLinearSpace; :: thesis: for L being additive Functional of V holds L . (0. V) = 0
let L be additive Functional of V; :: thesis: L . (0. V) = 0
(L . (0. V)) + 0 = L . ((0. V) + (0. V))
.= (L . (0. V)) + (L . (0. V)) by Def2 ;
hence L . (0. V) = 0 ; :: thesis: verum