let L, L9 be Linear_Combination of V; :: thesis: ( L = (- (1. GF)) * L9 implies L9 = (- (1. GF)) * L )
assume A1: L = (- (1. GF)) * L9 ; :: thesis: L9 = (- (1. GF)) * L
let v be Element of V; :: according to VECTSP_6:def 7 :: thesis: L9 . v = ((- (1. GF)) * L) . v
thus L9 . v = (1. GF) * (L9 . v)
.= ((1. GF) * (1. GF)) * (L9 . v)
.= ((- (1. GF)) * (- (1. GF))) * (L9 . v) by VECTSP_1:10
.= (((- (1. GF)) * (- (1. GF))) * L9) . v by Def9
.= ((- (1. GF)) * L) . v by A1, Th34 ; :: thesis: verum