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