let a, x be Element of R; :: according to IDEAL_1:def 2 :: thesis: ( not x in ker f or a * x in ker f )
assume AS: x in ker f ; :: thesis: a * x in ker f
f . (a * x) = (f . a) * (f . x) by GROUP_6:def 6
.= (f . a) * (0. S) by AS, ker1
.= 0. S ;
hence a * x in ker f ; :: thesis: verum