let L, L' be Linear_Combination of V; :: thesis: ( L = L' * (- (1_ R)) implies L' = L * (- (1_ R)) )
assume A1: L = L' * (- (1_ R)) ; :: thesis: L' = L * (- (1_ R))
let v be Vector of ; :: according to RMOD_4:def 10 :: thesis: L' . v = (L * (- (1_ R))) . v
thus L' . v = (L' . v) * (1_ R) by VECTSP_1:def 13
.= (L' . v) * ((1_ R) * (1_ R)) by VECTSP_1:def 13
.= (L' . v) * ((- (1_ R)) * (- (1_ R))) by VECTSP_1:42
.= (L' * ((- (1_ R)) * (- (1_ R)))) . v by Def12
.= (L * (- (1_ R))) . v by A1, Th64 ; :: thesis: verum