let L, K be Ring; :: thesis: for J being Function of K,L
for x being Scalar of K st J is linear holds
J . (- x) = - (J . x)
let J be Function of K,L; :: thesis: for x being Scalar of K st J is linear holds
J . (- x) = - (J . x)
let x be Scalar of K; :: thesis: ( J is linear implies J . (- x) = - (J . x) )
assume A1: J is linear ; :: thesis: J . (- x) = - (J . x)
then A2: J is additive by RINGCAT1:def 2;
set a = 0. K;
set b = 0. L;
set y = J . x;
A3: ( x + (- x) = 0. K & (J . x) + (- (J . x)) = 0. L ) by RLVECT_1:16;
then (J . x) + (J . (- x)) = J . (0. K) by A2, GRCAT_1:def 13
.= 0. L by A1, Lm7 ;
hence J . (- x) = - (J . x) by A3, RLVECT_1:21; :: thesis: verum