let K, L be Ring; :: thesis: for J being Function of K,L st J is additive holds
J . (0. K) = 0. L
let J be Function of K,L; :: thesis: ( J is additive implies J . (0. K) = 0. L )
set a = 0. K;
assume A1: J is additive ; :: thesis: J . (0. K) = 0. L
(0. K) + (0. K) = 0. K by RLVECT_1:4;
then (J . (0. K)) + (J . (0. K)) = J . (0. K) by A1
.= (J . (0. K)) + (0. L) by RLVECT_1:4 ;
hence J . (0. K) = 0. L by RLVECT_1:8; :: thesis: verum