let V be RealLinearSpace; :: thesis:
let M be Subset of V; :: thesis:
let L be Linear_Combination of M; :: thesis:
assume card (Carrier L) >= 1 ; :: thesis:
then Carrier L <> {} ;
then consider u being set such that
A1: u in Carrier L by XBOOLE_0:def 1;
reconsider u = u as VECTOR of V by A1;
consider L1 being Linear_Combination of {u} such that
A2: L1 . u = L . u from RLVECT_4:sch 2();
Carrier L c= M by RLVECT_2:def 8;
then A3: {u} c= M by A1, ZFMISC_1:37;
A4: Carrier L1 c= {u} by RLVECT_2:def 8;
then Carrier L1 c= M by A3, XBOOLE_1:1;
then reconsider L1 = L1 as Linear_Combination of M by RLVECT_2:def 8;
A5: for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v

proof

let v be VECTOR of V; :: thesis:
assume v in Carrier L1 ; :: thesis:
then v = u by A4, TARSKI:def 1;
hence L1 . v = L . v by A2; :: thesis:

end;

defpred S₁[ set , set ] means ( ( $1 in (Carrier L) \ {u} implies $2 = L . $1 ) & ( not $1 in (Carrier L) \ {u} implies $2 = 0 ) );
A7: for x being set st x in the carrier of V holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis:
assume x in the carrier of V ; :: thesis:
( x in (Carrier L) \ {u} or not x in (Carrier L) \ {u} ) ;
hence ex y being set st S₁[x,y] ; :: thesis:

end;

consider L2 being Function such that
A8: ( dom L2 = the carrier of V & ( for x being set st x in the carrier of V holds
S₁[x,L2 . x] ) ) from CLASSES1:sch 1(A7);
for y being set st y in rng L2 holds
y in REAL

proof

let y be set ; :: thesis:
assume y in rng L2 ; :: thesis:
then consider x being set such that
A9: ( x in dom L2 & y = L2 . x ) by FUNCT_1:def 5;

per cases ;

suppose A10: x in (Carrier L) \ {u} ; :: thesis:

then reconsider x = x as VECTOR of V ;
y = L . x by A8, A9, A10;
hence y in REAL ; :: thesis:

end;

suppose not x in (Carrier L) \ {u} ; :: thesis:

then y = 0 by A8, A9;
hence y in REAL ; :: thesis:

end;

then rng L2 c= REAL by TARSKI:def 3;
then A11: L2 is Element of Funcs the carrier of V,REAL by A8, FUNCT_2:def 2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds
L2 . v = 0

proof

set T = (Carrier L) \ {u};
reconsider T = (Carrier L) \ {u} as finite Subset of V ;
take T ; :: thesis:
thus for v being Element of V st not v in T holds
L2 . v = 0 by A8; :: thesis:

end;

then reconsider L2 = L2 as Linear_Combination of V by A11, RLVECT_2:def 5;
for x being set st x in Carrier L2 holds
x in M

proof

let x be set ; :: thesis:
assume A12: x in Carrier L2 ; :: thesis:
then reconsider x = x as VECTOR of V ;
L2 . x <> 0 by A12, RLVECT_2:28;
then x in (Carrier L) \ {u} by A8;
then A13: x in Carrier L by XBOOLE_0:def 5;
Carrier L c= M by RLVECT_2:def 8;
hence x in M by A13; :: thesis:

end;

then Carrier L2 c= M by TARSKI:def 3;
then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def 8;
Carrier L1 <> {}

proof

assume Carrier L1 = {} ; :: thesis:
then L . u = 0 by A2, RLVECT_2:28;
hence contradiction by A1, RLVECT_2:28; :: thesis:

end;

then A14: Carrier L1 = {u} by A4, ZFMISC_1:39;
for x being set st x in Carrier L2 holds
x in (Carrier L) \ {u}

proof

let x be set ; :: thesis:
assume A15: x in Carrier L2 ; :: thesis:
then reconsider x = x as VECTOR of V ;
L2 . x <> 0 by A15, RLVECT_2:28;
hence x in (Carrier L) \ {u} by A8; :: thesis:

end;

then A16: Carrier L2 c= (Carrier L) \ {u} by TARSKI:def 3;
for x being set st x in (Carrier L) \ {u} holds
x in Carrier L2

proof

let x be set ; :: thesis:
assume A17: x in (Carrier L) \ {u} ; :: thesis:
then reconsider x = x as VECTOR of V ;
A18: L2 . x = L . x by A8, A17;
x in Carrier L by A17, XBOOLE_0:def 5;
then L . x <> 0 by RLVECT_2:28;
hence x in Carrier L2 by A18, RLVECT_2:28; :: thesis:

end;

then (Carrier L) \ {u} c= Carrier L2 by TARSKI:def 3;
then A19: Carrier L2 = (Carrier L) \ {u} by A16, XBOOLE_0:def 10;
for v being VECTOR of V holds L . v = (L1 + L2) . v

proof

let v be VECTOR of V; :: thesis:

per cases ;

suppose A20: v in Carrier L ; :: thesis:

per cases ;

suppose A21: v = u ; :: thesis:

then A22: not v in Carrier L2 by A16, ZFMISC_1:64;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def 12
.= (L . v) + 0 by A2, A21, A22, RLVECT_2:28 ;
hence L . v = (L1 + L2) . v ; :: thesis:

end;

suppose A23: v <> u ; :: thesis:

then not v in Carrier L1 by A4, TARSKI:def 1;
then A24: L1 . v = 0 by RLVECT_2:28;
A25: v in (Carrier L) \ {u} by A20, A23, ZFMISC_1:64;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def 12
.= 0 + (L . v) by A8, A24, A25 ;
hence L . v = (L1 + L2) . v ; :: thesis:

end;

suppose A26: not v in Carrier L ; :: thesis:

then A27: not v in Carrier L1 by A1, A4, TARSKI:def 1;
not v in Carrier L2 by A16, A26, ZFMISC_1:64;
then A28: L2 . v = 0 by RLVECT_2:28;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def 12
.= 0 by A27, A28, RLVECT_2:28 ;
hence L . v = (L1 + L2) . v by A26, RLVECT_2:28; :: thesis:

end;

then A29: L = L1 + L2 by RLVECT_2:def 11;
Carrier L1 c= Carrier L by A1, A14, ZFMISC_1:37;
then A30: card (Carrier L2) = (card (Carrier L)) - (card (Carrier L1)) by A14, A19, CARD_2:63
.= (card (Carrier L)) - 1 by A14, CARD_1:50 ;
take L1 ; :: thesis:
take L2 ; :: thesis:
(Carrier L) \ {u} c= Carrier L by XBOOLE_1:36;
hence ( Sum L = (Sum L1) + (Sum L2) & card (Carrier L1) = 1 & card (Carrier L2) = (card (Carrier L)) - 1 & Carrier L1 c= Carrier L & Carrier L2 c= Carrier L & ( for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v ) & ( for v being VECTOR of V st v in Carrier L2 holds
L2 . v = L . v ) ) by A1, A5, A8, A14, A16, A29, A30, CARD_1:50, RLVECT_3:1, XBOOLE_1:1, ZFMISC_1:37; :: thesis: