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

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