let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for L being non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr
for J being Function of K,L st J is linear holds
opp J is additive
let L be non empty right_complementable well-unital add-associative right_zeroed doubleLoopStr ; :: thesis: for J being Function of K,L st J is linear holds
opp J is additive
let J be Function of K,L; :: thesis: ( J is linear implies opp J is additive )
set J9 = opp J;
assume A1: J is linear ; :: thesis: opp J is additive
let x, y be Scalar of K; :: according to VECTSP_1:def 19 :: thesis: (opp J) . (x + y) = ((opp J) . x) + ((opp J) . y)
thus (opp J) . (x + y) = (J . x) + (J . y) by A1, VECTSP_1:def 20
.= ((opp J) . x) + ((opp J) . y) ; :: thesis: verum