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

hence
for bL1 = 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

end;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

hence
L1 = L2
; :: thesis: verumlet 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;thus L1 . v = LR . ((r ") * v) by A8

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

( ( r <> 0 & ( for v being Element of R holds b