let K, L be Ring; :: thesis: for J being Function of K,L st J is linear holds
J . (0. K) = 0. L
let J be Function of K,L; :: thesis: ( J is linear implies J . (0. K) = 0. L )
set a = 0. K;
assume J is linear ; :: thesis: J . (0. K) = 0. L
then A1: J is additive by RINGCAT1:def 2;
(0. K) + (0. K) = 0. K by RLVECT_1:10;
then (J . (0. K)) + (J . (0. K)) = J . (0. K) by A1, GRCAT_1:def 13
.= (J . (0. K)) + (0. L) by RLVECT_1:10 ;
hence J . (0. K) = 0. L by RLVECT_1:21; :: thesis: verum