let K, L be Ring; :: thesis: for J being Function of K,L
for x, y being Scalar of K st J is antilinear holds
J . (x - y) = (J . x) - (J . y)
let J be Function of K,L; :: thesis: for x, y being Scalar of K st J is antilinear holds
J . (x - y) = (J . x) - (J . y)
let x, y be Scalar of K; :: thesis: ( J is antilinear implies J . (x - y) = (J . x) - (J . y) )
assume A1: J is antilinear ; :: thesis: J . (x - y) = (J . x) - (J . y)
hence J . (x - y) = (J . x) + (J . (- y)) by VECTSP_1:def 20
.= (J . x) - (J . y) by A1, Lm10 ;
:: thesis: verum