let L1, L2 be Linear_Combination of V; :: thesis: ( ( for v being VECTOR of V holds L1 . v = i * (L . v) ) & ( for v being VECTOR of V holds L2 . v = i * (L . v) ) implies L1 = L2 )
assume that
A3: for v being VECTOR of V holds L1 . v = i * (L . v) and
A4: for v being VECTOR of V holds L2 . v = i * (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 = i * (L . v) by A3
.= L2 . v by A4 ; :: thesis: verum