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

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