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