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

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