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

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

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

let v be Element of V; :: according to VECTSP_6:def 7 :: thesis: L1 . v = L2 . v

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

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

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

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

let v be Element of V; :: according to VECTSP_6:def 7 :: thesis: L1 . v = L2 . v

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

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