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 object 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 by RLVECT_4:37;
A3: Carrier L1 c= {u} by RLVECT_2:def 6;
Carrier L c= M by RLVECT_2:def 6;
then {u} c= M by A1, ZFMISC_1:31;
then Carrier L1 c= M by A3;
then reconsider L1 = L1 as Linear_Combination of M by RLVECT_2:def 6;
A4: for v being VECTOR of V st v in Carrier L1 holds
L1 . v = L . v

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

end;

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

proof

let x be object ; :: 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 object st S₁[x,y] ; :: thesis:

end;

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

proof

let y be object ; :: thesis:
assume y in rng L2 ; :: thesis:
then consider x being object such that
A7: x in dom L2 and
A8: y = L2 . x by FUNCT_1:def 3;

per cases ;

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

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

end;

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

then y = In (0,REAL) by A6, A7, A8;
hence y in REAL ; :: thesis:

end;

then rng L2 c= REAL ;
then A10: L2 is Element of Funcs ( the carrier of V,REAL) by A6, 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 A6; :: thesis:

end;

then reconsider L2 = L2 as Linear_Combination of V by A10, RLVECT_2:def 3;
for x being object st x in Carrier L2 holds
x in M

proof

let x be object ; :: thesis:
assume A11: x in Carrier L2 ; :: thesis:
then reconsider x = x as VECTOR of V ;
L2 . x <> 0 by A11, RLVECT_2:19;
then x in (Carrier L) \ {u} by A6;
then A12: x in Carrier L by XBOOLE_0:def 5;
Carrier L c= M by RLVECT_2:def 6;
hence x in M by A12; :: thesis:

end;

then Carrier L2 c= M ;
then reconsider L2 = L2 as Linear_Combination of M by RLVECT_2:def 6;
for x being object st x in Carrier L2 holds
x in (Carrier L) \ {u}

proof

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

end;

then A14: Carrier L2 c= (Carrier L) \ {u} ;
for v being VECTOR of V holds L . v = (L1 + L2) . v

proof

let v be VECTOR of V; :: thesis:

per cases ;

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

per cases ;

suppose A16: v = u ; :: thesis:

then A17: not v in Carrier L2 by A14, ZFMISC_1:56;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def 10
.= (L . v) + 0 by A2, A16, A17, RLVECT_2:19 ;
hence L . v = (L1 + L2) . v ; :: thesis:

end;

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

then not v in Carrier L1 by A3, TARSKI:def 1;
then A19: L1 . v = 0 by RLVECT_2:19;
A20: v in (Carrier L) \ {u} by A15, A18, ZFMISC_1:56;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def 10
.= 0 + (L . v) by A6, A19, A20 ;
hence L . v = (L1 + L2) . v ; :: thesis:

end;

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

then not v in Carrier L2 by A14, ZFMISC_1:56;
then A22: L2 . v = 0 by RLVECT_2:19;
A23: not v in Carrier L1 by A1, A3, A21, TARSKI:def 1;
(L1 + L2) . v = (L1 . v) + (L2 . v) by RLVECT_2:def 10
.= 0 by A23, A22, RLVECT_2:19 ;
hence L . v = (L1 + L2) . v by A21, RLVECT_2:19; :: thesis:

end;

then A24: L = L1 + L2 by RLVECT_2:def 9;
for x being object st x in (Carrier L) \ {u} holds
x in Carrier L2

proof

let x be object ; :: thesis:
assume A25: x in (Carrier L) \ {u} ; :: thesis:
then reconsider x = x as VECTOR of V ;
x in Carrier L by A25, XBOOLE_0:def 5;
then A26: L . x <> 0 by RLVECT_2:19;
L2 . x = L . x by A6, A25;
hence x in Carrier L2 by A26, RLVECT_2:19; :: thesis:

end;

then (Carrier L) \ {u} c= Carrier L2 ;
then A27: Carrier L2 = (Carrier L) \ {u} by A14, XBOOLE_0:def 10;
take L1 ; :: thesis:
take L2 ; :: thesis:
A28: (Carrier L) \ {u} c= Carrier L by XBOOLE_1:36;
Carrier L1 <> {}

proof

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

end;

then A29: Carrier L1 = {u} by A3, ZFMISC_1:33;
then Carrier L1 c= Carrier L by A1, ZFMISC_1:31;
then card (Carrier L2) = (card (Carrier L)) - (card (Carrier L1)) by A29, A27, CARD_2:44
.= (card (Carrier L)) - 1 by A29, CARD_1:30 ;
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, A4, A6, A29, A14, A24, A28, CARD_1:30, RLVECT_3:1, ZFMISC_1:31; :: thesis: