let r be Real; :: thesis:
let V be RealLinearSpace; :: thesis:
let Af be finite Subset of V; :: thesis:
set cV = the carrier of V;
set Ar = (ZeroLC V) +* (Af --> r);
A1: dom (Af --> r) = Af ;
dom (ZeroLC V) = the carrier of V by FUNCT_2:def 1;
then dom ((ZeroLC V) +* (Af --> r)) = the carrier of V \/ Af by A1, FUNCT_4:def 1;
then ( rng ((ZeroLC V) +* (Af --> r)) c= (rng (Af --> r)) \/ (rng (ZeroLC V)) & dom ((ZeroLC V) +* (Af --> r)) = the carrier of V ) by FUNCT_4:17, XBOOLE_1:12;
then (ZeroLC V) +* (Af --> r) is Function of the carrier of V,REAL by FUNCT_2:2;
then reconsider Ar = (ZeroLC V) +* (Af --> r) as Element of Funcs ( the carrier of V,REAL) by FUNCT_2:8;

take Af = Af; :: thesis:
let v be VECTOR of V; :: thesis:
assume not v in Af ; :: thesis:
hence Ar . v = (ZeroLC V) . v by A1, FUNCT_4:11
.= 0 by RLVECT_2:20 ;
:: thesis:

end;

then reconsider Ar = Ar as Linear_Combination of V by RLVECT_2:def 3;
Carrier Ar c= Af

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in Carrier Ar ; :: thesis:
then reconsider v = x as Element of V ;
assume not x in Af ; :: thesis:
then Ar . x = (ZeroLC V) . v by A1, FUNCT_4:11
.= 0 by RLVECT_2:20 ;
hence contradiction by A2, RLVECT_2:19; :: thesis:

end;

then reconsider Ar = (ZeroLC V) +* (Af --> r) as Linear_Combination of Af by RLVECT_2:def 6;
A3: Carrier Ar c= Af by RLVECT_2:def 6;

suppose A4: r = 0 ; :: thesis:

Carrier Ar = {}

assume Carrier Ar <> {} ; :: thesis:
then consider x being object such that
A5: x in Carrier Ar by XBOOLE_0:def 1;
( Ar . x = (Af --> r) . x & (Af --> r) . x = 0 ) by A1, A3, A4, A5, FUNCOP_1:7, FUNCT_4:13;
hence contradiction by A5, RLVECT_2:19; :: thesis:

end;

then Ar = ZeroLC V by RLVECT_2:def 5;
then A6: ( Sum Ar = 0. V & sum Ar = 0 ) by RLAFFIN1:31, RLVECT_2:30;
r * (Sum Af) = 0. V by A4, RLVECT_1:10;
hence ex L being Linear_Combination of Af st
( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) by A4, A6; :: thesis:

end;

suppose A7: r <> 0 ; :: thesis:

consider F being FinSequence of V such that
A8: F is one-to-one and
A9: rng F = Carrier Ar and
A10: Sum Ar = Sum (Ar (#) F) by RLVECT_2:def 8;
reconsider r = r as Element of REAL by XREAL_0:def 1;
Af c= Carrier Ar

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A11: x in Af ; :: thesis:
then Ar . x = (Af --> r) . x by A1, FUNCT_4:13;
hence x in Carrier Ar by A7, A11; :: thesis:

end;

then A12: Af = Carrier Ar by A3;
then dom F,Af are_equipotent by A8, A9, WELLORD2:def 4;
then A13: card Af = card (dom F) by CARD_1:5
.= card (Seg (len F)) by FINSEQ_1:def 3
.= len F by FINSEQ_1:57 ;
set L = (len F) |-> r;
A14: len (Ar * F) = len F by FINSEQ_2:33;
then reconsider ArF = Ar * F as Element of (len F) -tuples_on REAL by FINSEQ_2:92;

let i be Nat; :: thesis:
assume A15: i in Seg (len F) ; :: thesis:
then i in dom F by FINSEQ_1:def 3;
then A16: F . i in rng F by FUNCT_1:def 3;
then A17: (Af --> r) . (F . i) = r by A3, A9, FUNCOP_1:7;
i in dom ArF by A14, A15, FINSEQ_1:def 3;
then ArF . i = Ar . (F . i) by FUNCT_1:12;
then ArF . i = (Af --> r) . (F . i) by A1, A3, A9, A16, FUNCT_4:13;
hence ArF . i = ((len F) |-> r) . i by A15, A17, FINSEQ_2:57; :: thesis:

end;

then ArF = (len F) |-> r by FINSEQ_2:119;
then A18: sum Ar = Sum ((len F) |-> r) by A8, A9, RLAFFIN1:def 3
.= (len F) * r by RVSUM_1:80 ;
set AF = Ar (#) F;
A19: len (Ar (#) F) = len F by RLVECT_2:def 7;
then A20: dom (Ar (#) F) = dom F by FINSEQ_3:29;

let i be Nat; :: thesis:
assume A21: i in dom F ; :: thesis:
then ( F /. i = F . i & F . i in rng F ) by FUNCT_1:def 3, PARTFUN1:def 6;
then ( Ar . (F /. i) = (Af --> r) . (F /. i) & (Af --> r) . (F /. i) = r ) by A1, A3, A9, FUNCOP_1:7, FUNCT_4:13;
hence (Ar (#) F) . i = r * (F /. i) by A20, A21, RLVECT_2:def 7; :: thesis:

end;

then Sum Ar = r * (Sum F) by A10, A19, RLVECT_2:3
.= r * (Sum Af) by A8, A9, A12, RLVECT_2:def 2 ;
hence ex L being Linear_Combination of Af st
( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) ) by A13, A18; :: thesis:

end;

end;