let x, y be Element of R; :: according to IDEAL_1:def 1 :: thesis: ( not x in ker f or not y in ker f or x + y in ker f )
assume AS: ( x in ker f & y in ker f ) ; :: thesis: x + y in ker f
f . (x + y) = (f . x) + (f . y) by VECTSP_1:def 20
.= (0. S) + (f . y) by AS, ker1
.= 0. S by AS, ker1 ;
hence x + y in ker f ; :: thesis: verum