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
A1: Sum L1 = x and
A2: sum L1 = 1 and
A3: Sum L2 = x and
A4: sum L2 = 1 ; :: thesis: L1 = L2
A5: Sum (L1 - L2) = (Sum L1) - (Sum L1) by A1, A3, RLVECT_3:4
.= 0. V by RLVECT_1:15 ;
A6: L1 - L2 is Linear_Combination of A by RLVECT_2:56;
sum (L1 - L2) = 1 - 1 by A2, A4, Th36
.= 0 ;
then Carrier (L1 - L2) = {} by B1, A5, A6, Th42;
then ZeroLC V = L1 + (- L2) by RLVECT_2:def 5;
then A7: - L2 = - L1 by RLVECT_2:50;
L1 = - (- L1) by RLVECT_2:53;
hence L1 = L2 by A7, RLVECT_2:53; :: thesis: verum