let L1, L2 be Linear_Combination of A; :: thesis: ( Sum L1 = x & sum L1 = 1 & Sum L2 = x & sum L2 = 1 implies L1 = L2 )
assume that
A3: Sum L1 = x and
A4: sum L1 = 1 and
A5: Sum L2 = x and
A6: sum L2 = 1 ; :: thesis: L1 = L2
A7: Sum (L1 - L2) = (Sum L1) - (Sum L1) by A3, A5, RLVECT_3:4
.= 0. V by RLVECT_1:15 ;
A8: L1 - L2 is Linear_Combination of A by RLVECT_2:56;
sum (L1 - L2) = 1 - 1 by A4, A6, Th36
.= 0 ;
then Carrier (L1 - L2) = {} by A1, A7, A8, Th42;
then ZeroLC V = L1 + (- L2) by RLVECT_2:def 5;
then A9: - L2 = - L1 by RLVECT_2:50;
L1 = - (- L1) by RLVECT_2:53;
hence L1 = L2 by A9, RLVECT_2:53; :: thesis: verum