now :: thesis: for L1, L2 being Linear_Combination of R st ( for v being Element of R holds L1 . v = LR . ((r ") * v) ) & ( for v being Element of R holds L2 . v = LR . ((r ") * v) ) holds
L1 = L2

let L1, L2 be Linear_Combination of R; :: thesis: ( ( for v being Element of R holds L1 . v = LR . ((r ") * v) ) & ( for v being Element of R holds L2 . v = LR . ((r ") * v) ) implies L1 = L2 )
assume that
A8: for v being Element of R holds L1 . v = LR . ((r ") * v) and
A9: for v being Element of R holds L2 . v = LR . ((r ") * v) ; :: thesis: L1 = L2

now :: thesis: for v being Element of R holds L1 . v = L2 . v

let v be Element of R; :: thesis: L1 . v = L2 . v
thus L1 . v = LR . ((r ") * v) by A8
.= L2 . v by A9 ; :: thesis: verum

end;

hence L1 = L2 ; :: thesis: verum

end;

hence for b₁, b₂ being Linear_Combination of R holds
( ( r <> 0 & ( for v being Element of R holds b₁ . v = LR . ((r ") * v) ) & ( for v being Element of R holds b₂ . v = LR . ((r ") * v) ) implies b₁ = b₂ ) & ( not r <> 0 & b₁ = ZeroLC R & b₂ = ZeroLC R implies b₁ = b₂ ) ) ; :: thesis: verum