let V be RealLinearSpace; :: thesis: for KL1, KL2 being Linear_Combination of V

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

let KL1, KL2 be Linear_Combination of V; :: thesis: for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

let X be Subset of V; :: thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 implies KL1 = KL2 )

assume A1: X is linearly-independent ; :: thesis: ( not Carrier KL1 c= X or not Carrier KL2 c= X or not Sum KL1 = Sum KL2 or KL1 = KL2 )

assume A2: Carrier KL1 c= X ; :: thesis: ( not Carrier KL2 c= X or not Sum KL1 = Sum KL2 or KL1 = KL2 )

assume Carrier KL2 c= X ; :: thesis: ( not Sum KL1 = Sum KL2 or KL1 = KL2 )

then A3: (Carrier KL1) \/ (Carrier KL2) c= X by A2, XBOOLE_1:8;

assume Sum KL1 = Sum KL2 ; :: thesis: KL1 = KL2

then (Sum KL1) - (Sum KL2) = (Sum KL1) + (- (Sum KL1)) by RLVECT_1:def 11

.= 0. V by RLVECT_1:5 ;

then A4: ( KL1 - KL2 is Linear_Combination of Carrier (KL1 - KL2) & Sum (KL1 - KL2) = 0. V ) by RLVECT_2:def 6, RLVECT_3:4;

Carrier (KL1 - KL2) c= (Carrier KL1) \/ (Carrier KL2) by RLVECT_2:55;

then A5: Carrier (KL1 - KL2) is linearly-independent by A1, A3, RLVECT_3:5, XBOOLE_1:1;

for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

let KL1, KL2 be Linear_Combination of V; :: thesis: for X being Subset of V st X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 holds

KL1 = KL2

let X be Subset of V; :: thesis: ( X is linearly-independent & Carrier KL1 c= X & Carrier KL2 c= X & Sum KL1 = Sum KL2 implies KL1 = KL2 )

assume A1: X is linearly-independent ; :: thesis: ( not Carrier KL1 c= X or not Carrier KL2 c= X or not Sum KL1 = Sum KL2 or KL1 = KL2 )

assume A2: Carrier KL1 c= X ; :: thesis: ( not Carrier KL2 c= X or not Sum KL1 = Sum KL2 or KL1 = KL2 )

assume Carrier KL2 c= X ; :: thesis: ( not Sum KL1 = Sum KL2 or KL1 = KL2 )

then A3: (Carrier KL1) \/ (Carrier KL2) c= X by A2, XBOOLE_1:8;

assume Sum KL1 = Sum KL2 ; :: thesis: KL1 = KL2

then (Sum KL1) - (Sum KL2) = (Sum KL1) + (- (Sum KL1)) by RLVECT_1:def 11

.= 0. V by RLVECT_1:5 ;

then A4: ( KL1 - KL2 is Linear_Combination of Carrier (KL1 - KL2) & Sum (KL1 - KL2) = 0. V ) by RLVECT_2:def 6, RLVECT_3:4;

Carrier (KL1 - KL2) c= (Carrier KL1) \/ (Carrier KL2) by RLVECT_2:55;

then A5: Carrier (KL1 - KL2) is linearly-independent by A1, A3, RLVECT_3:5, XBOOLE_1:1;

now :: thesis: for v being VECTOR of V holds KL1 . v = KL2 . v

hence
KL1 = KL2
by RLVECT_2:def 9; :: thesis: verumlet v be VECTOR of V; :: thesis: KL1 . v = KL2 . v

not v in Carrier (KL1 - KL2) by A5, A4, RLVECT_3:def 1;

then (KL1 - KL2) . v = 0 by RLVECT_2:19;

then (KL1 . v) - (KL2 . v) = 0 by RLVECT_2:54;

hence KL1 . v = KL2 . v ; :: thesis: verum

end;not v in Carrier (KL1 - KL2) by A5, A4, RLVECT_3:def 1;

then (KL1 - KL2) . v = 0 by RLVECT_2:19;

then (KL1 . v) - (KL2 . v) = 0 by RLVECT_2:54;

hence KL1 . v = KL2 . v ; :: thesis: verum