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

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