let K, L be Ring; :: thesis: for J being Function of K,L

for x being Scalar of K st J is antilinear holds

J . (- x) = - (J . x)

let J be Function of K,L; :: thesis: for x being Scalar of K st J is antilinear holds

J . (- x) = - (J . x)

let x be Scalar of K; :: thesis: ( J is antilinear implies J . (- x) = - (J . x) )

assume A1: J is antilinear ; :: thesis: J . (- x) = - (J . x)

set a = 0. K;

set b = 0. L;

set y = J . x;

A2: (J . x) + (- (J . x)) = 0. L by RLVECT_1:5;

x + (- x) = 0. K by RLVECT_1:5;

then (J . x) + (J . (- x)) = J . (0. K) by A1, VECTSP_1:def 20

.= 0. L by A1, Lm9 ;

hence J . (- x) = - (J . x) by A2, RLVECT_1:8; :: thesis: verum

for x being Scalar of K st J is antilinear holds

J . (- x) = - (J . x)

let J be Function of K,L; :: thesis: for x being Scalar of K st J is antilinear holds

J . (- x) = - (J . x)

let x be Scalar of K; :: thesis: ( J is antilinear implies J . (- x) = - (J . x) )

assume A1: J is antilinear ; :: thesis: J . (- x) = - (J . x)

set a = 0. K;

set b = 0. L;

set y = J . x;

A2: (J . x) + (- (J . x)) = 0. L by RLVECT_1:5;

x + (- x) = 0. K by RLVECT_1:5;

then (J . x) + (J . (- x)) = J . (0. K) by A1, VECTSP_1:def 20

.= 0. L by A1, Lm9 ;

hence J . (- x) = - (J . x) by A2, RLVECT_1:8; :: thesis: verum