let M, N be Linear_Combination of V; :: thesis: ( ( for v being Element of V holds M . v = (L1 . v) + (L2 . v) ) & ( for v being Element of V holds N . v = (L1 . v) + (L2 . v) ) implies M = N )
assume A4: for v being Element of V holds M . v = (L1 . v) + (L2 . v) ; :: thesis: ( ex v being Element of V st not N . v = (L1 . v) + (L2 . v) or M = N )
assume A5: for v being Element of V holds N . v = (L1 . v) + (L2 . v) ; :: thesis: M = N
let v be Element of V; :: according to VECTSP_6:def 10 :: thesis: M . v = N . v
thus M . v = (L1 . v) + (L2 . v) by A4
.= N . v by A5 ; :: thesis: verum