let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for S being non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr
for f being additive Function of R,S
for x being Element of R holds f . (- x) = - (f . x)
let S be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for f being additive Function of R,S
for x being Element of R holds f . (- x) = - (f . x)
let f be additive Function of R,S; :: thesis: for x being Element of R holds f . (- x) = - (f . x)
let x be Element of R; :: thesis: f . (- x) = - (f . x)
0. S = f . (0. R) by hom1
.= f . ((- x) + x) by RLVECT_1:5
.= (f . (- x)) + (f . x) by VECTSP_1:def 20 ;
hence f . (- x) = - (f . x) by RLVECT_1:6; :: thesis: verum