let L, L9 be Linear_Combination of V; :: thesis: ( L = L9 * (- (1_ R)) implies L9 = L * (- (1_ R)) )
assume A1: L = L9 * (- (1_ R)) ; :: thesis: L9 = L * (- (1_ R))
let v be Vector of V; :: according to RMOD_4:def 8 :: thesis: L9 . v = (L * (- (1_ R))) . v
thus L9 . v = (L9 . v) * (1_ R)
.= (L9 . v) * ((1_ R) * (1_ R))
.= (L9 . v) * ((- (1_ R)) * (- (1_ R))) by VECTSP_1:10
.= (L9 * ((- (1_ R)) * (- (1_ R)))) . v by Def10
.= (L * (- (1_ R))) . v by A1, Th48 ; :: thesis: verum