let V be RealLinearSpace; :: thesis: 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
let L1, L2 be Linear_Combination of V; :: thesis: ( Sum L1 <> Sum L2 & sum L1 = sum L2 implies ex v being VECTOR of V st L1 . v > L2 . v )
assume that
A1: Sum L1 <> Sum L2 and
A2: sum L1 = sum L2 ; :: thesis: ex v being VECTOR of V st L1 . v > L2 . v
consider F being FinSequence such that
A3: rng F = (Carrier L1) \/ (Carrier L2) and
A4: F is one-to-one by FINSEQ_4:58;
reconsider F = F as FinSequence of V by A3, FINSEQ_1:def 4;
A5: len (L2 * F) = len F by FINSEQ_2:33;
A6: len (L1 * F) = len F by FINSEQ_2:33;
then reconsider L1F = L1 * F, L2F = L2 * F as Element of (len F) -tuples_on REAL by A5, FINSEQ_2:92;
A7: len (L2F - L1F) = len F by CARD_1:def 7;
assume A8: for v being Element of V holds L1 . v <= L2 . v ; :: thesis: contradiction
A9: for i being Nat st i in dom (L2F - L1F) holds
0 <= (L2F - L1F) . i

proof

let i be Nat; :: thesis: ( i in dom (L2F - L1F) implies 0 <= (L2F - L1F) . i )
L2 . (F /. i) >= L1 . (F /. i) by A8;
then A10: (L2 . (F /. i)) - (L1 . (F /. i)) >= (L1 . (F /. i)) - (L1 . (F /. i)) by XREAL_1:9;
assume A11: i in dom (L2F - L1F) ; :: thesis: 0 <= (L2F - L1F) . i
then i in dom F by A7, FINSEQ_3:29;
then A12: F /. i = F . i by PARTFUN1:def 6;
i in dom L2F by A5, A7, A11, FINSEQ_3:29;
then A13: L2F . i = L2 . (F . i) by FUNCT_1:12;
i in dom L1F by A6, A7, A11, FINSEQ_3:29;
then L1F . i = L1 . (F . i) by FUNCT_1:12;
hence 0 <= (L2F - L1F) . i by A10, A12, A13, RVSUM_1:27; :: thesis: verum

end;

A14: Sum (L2F - L1F) = (Sum L2F) - (Sum L1F) by RVSUM_1:90
.= (sum L2) - (Sum L1F) by A3, A4, RLAFFIN1:30, XBOOLE_1:7
.= (sum L2) - (sum L1) by A3, A4, RLAFFIN1:30, XBOOLE_1:7
.= 0 by A2 ;

now :: thesis: for v being Element of V holds L1 . v = L2 . v

let v be Element of V; :: thesis: L1 . v = L2 . v

now :: thesis: L1 . v = L2 . v

per cases ( ( not v in Carrier L1 & not v in Carrier L2 ) or v in rng F ) by A3, XBOOLE_0:def 3;

suppose A15: ( not v in Carrier L1 & not v in Carrier L2 ) ; :: thesis: L1 . v = L2 . v

then L1 . v = 0 ;
hence L1 . v = L2 . v by A15; :: thesis: verum

end;

suppose v in rng F ; :: thesis: L1 . v = L2 . v

then consider i being object such that
A16: i in dom F and
A17: F . i = v by FUNCT_1:def 3;
reconsider i = i as Nat by A16;
i in dom L2F by A5, A16, FINSEQ_3:29;
then A18: ( (L2F - L1F) . i = (L2F . i) - (L1F . i) & L2F . i = L2 . v ) by A17, FUNCT_1:12, RVSUM_1:27;
i in dom L1F by A6, A16, FINSEQ_3:29;
then A19: L1F . i = L1 . v by A17, FUNCT_1:12;
A20: i in dom (L2F - L1F) by A7, A16, FINSEQ_3:29;
then (L2 . v) - (L1 . v) <= 0 by A9, A14, A18, A19, RVSUM_1:85;
then (L2 . v) - (L1 . v) = 0 by A9, A18, A19, A20;
hence L1 . v = L2 . v ; :: thesis: verum

end;

end;

end;

hence L1 . v = L2 . v ; :: thesis: verum

end;

hence contradiction by A1, RLVECT_2:def 9; :: thesis: verum