theorem Th24: :: RLAFFIN2:24

for V being RealLinearSpace
for L1, L2 being Linear_Combination of V st Sum L1 <> Sum L2 & sum L1 = sum L2 holds
ex v being VECTOR of V st L1 . v > L2 . v