let L, L' be Linear_Combination of V; :: thesis: ( L = (- (1. GF)) * L' implies L' = (- (1. GF)) * L )
assume A1: L = (- (1. GF)) * L' ; :: thesis: L' = (- (1. GF)) * L
let v be Element of V; :: according to VECTSP_6:def 10 :: thesis: L' . v = ((- (1. GF)) * L) . v
thus L' . v = (1. GF) * (L' . v) by VECTSP_1:def 19
.= ((1. GF) * (1. GF)) * (L' . v) by VECTSP_1:def 19
.= ((- (1. GF)) * (- (1. GF))) * (L' . v) by VECTSP_1:42
.= (((- (1. GF)) * (- (1. GF))) * L') . v by Def12
.= ((- (1. GF)) * L) . v by A1, Th64 ; :: thesis: verum