let L1, L2 be Linear_Combination of V; :: thesis: ( ( for v being VECTOR of V holds L1 . v = a * (L . v) ) & ( for v being VECTOR of V holds L2 . v = a * (L . v) ) implies L1 = L2 )

assume A3: for v being VECTOR of V holds L1 . v = a * (L . v) ; :: thesis: ( ex v being VECTOR of V st not L2 . v = a * (L . v) or L1 = L2 )

assume A4: for v being VECTOR of V holds L2 . v = a * (L . v) ; :: thesis: L1 = L2

let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: L1 . v = L2 . v

thus L1 . v = a * (L . v) by A3

.= L2 . v by A4 ; :: thesis: verum

assume A3: for v being VECTOR of V holds L1 . v = a * (L . v) ; :: thesis: ( ex v being VECTOR of V st not L2 . v = a * (L . v) or L1 = L2 )

assume A4: for v being VECTOR of V holds L2 . v = a * (L . v) ; :: thesis: L1 = L2

let v be VECTOR of V; :: according to RLVECT_2:def 9 :: thesis: L1 . v = L2 . v

thus L1 . v = a * (L . v) by A3

.= L2 . v by A4 ; :: thesis: verum