let L1, L be Z_Linear_Combination of V; :: thesis: ( L1 = (- 1) * L implies L = (- 1) * L1 )
assume A1: L1 = (- 1) * L ; :: thesis: L = (- 1) * L1
1 * L = ((- 1) * (- 1)) * L
.= (- 1) * ((- 1) * L) by Th34 ;
hence L = (- 1) * L1 by A1; :: thesis: verum