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 b1, b2 being Linear_Combination of R holds
( ( r <> 0 & ( for v being Element of R holds b1 . v = LR . ((r ") * v) ) & ( for v being Element of R holds b2 . v = LR . ((r ") * v) ) implies b1 = b2 ) & ( not r <> 0 & b1 = ZeroLC R & b2 = ZeroLC R implies b1 = b2 ) ) ; :: thesis: verum