let L1, L2 be Linear_Combination of V; ( ( for v being Vector of V holds L1 . v = (L . v) * a ) & ( for v being Vector of V holds L2 . v = (L . v) * a ) implies L1 = L2 )
assume A2:
for v being Vector of V holds L1 . v = (L . v) * a
; ( ex v being Vector of V st not L2 . v = (L . v) * a or L1 = L2 )
assume A3:
for v being Vector of V holds L2 . v = (L . v) * a
; L1 = L2
let v be Vector of V; RMOD_4:def 8 L1 . v = L2 . v
thus L1 . v =
(L . v) * a
by A2
.=
L2 . v
by A3
; verum