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