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

for x, y being Scalar of K st J is linear 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 linear holds

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

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

assume A1: J is linear ; :: 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, Lm7 ;

:: thesis: verum

for x, y being Scalar of K st J is linear 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 linear holds

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

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

assume A1: J is linear ; :: 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, Lm7 ;

:: thesis: verum