let r be Real; :: thesis: for V being RealLinearSpace

for Af being finite Subset of V ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

let V be RealLinearSpace; :: thesis: for Af being finite Subset of V ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

let Af be finite Subset of V; :: thesis: ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

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;

Carrier Ar c= Af

A3: Carrier Ar c= Af by RLVECT_2:def 6;

for Af being finite Subset of V ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

let V be RealLinearSpace; :: thesis: for Af being finite Subset of V ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

let Af be finite Subset of V; :: thesis: ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

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;

now :: thesis: ex Af being finite Subset of V st

for v being VECTOR of V st not v in Af holds

Ar . v = 0

then reconsider Ar = Ar as Linear_Combination of V by RLVECT_2:def 3;for v being VECTOR of V st not v in Af holds

Ar . v = 0

take Af = Af; :: thesis: for v being VECTOR of V st not v in Af holds

Ar . v = 0

let v be VECTOR of V; :: thesis: ( not v in Af implies Ar . v = 0 )

assume not v in Af ; :: thesis: Ar . v = 0

hence Ar . v = (ZeroLC V) . v by A1, FUNCT_4:11

.= 0 by RLVECT_2:20 ;

:: thesis: verum

end;Ar . v = 0

let v be VECTOR of V; :: thesis: ( not v in Af implies Ar . v = 0 )

assume not v in Af ; :: thesis: Ar . v = 0

hence Ar . v = (ZeroLC V) . v by A1, FUNCT_4:11

.= 0 by RLVECT_2:20 ;

:: thesis: verum

Carrier Ar c= Af

proof

then reconsider Ar = (ZeroLC V) +* (Af --> r) as Linear_Combination of Af by RLVECT_2:def 6;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier Ar or x in Af )

assume A2: x in Carrier Ar ; :: thesis: x in Af

then reconsider v = x as Element of V ;

assume not x in Af ; :: thesis: contradiction

then Ar . x = (ZeroLC V) . v by A1, FUNCT_4:11

.= 0 by RLVECT_2:20 ;

hence contradiction by A2, RLVECT_2:19; :: thesis: verum

end;assume A2: x in Carrier Ar ; :: thesis: x in Af

then reconsider v = x as Element of V ;

assume not x in Af ; :: thesis: contradiction

then Ar . x = (ZeroLC V) . v by A1, FUNCT_4:11

.= 0 by RLVECT_2:20 ;

hence contradiction by A2, RLVECT_2:19; :: thesis: verum

A3: Carrier Ar c= Af by RLVECT_2:def 6;

per cases
( r = 0 or r <> 0 )
;

end;

suppose A4:
r = 0
; :: thesis: ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

Carrier Ar = {}

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: verum

end;proof

then
Ar = ZeroLC V
by RLVECT_2:def 5;
assume
Carrier Ar <> {}
; :: thesis: contradiction

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: verum

end;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: verum

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: verum

suppose A7:
r <> 0
; :: thesis: ex L being Linear_Combination of Af st

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

( Sum L = r * (Sum Af) & sum L = r * (card Af) & L = (ZeroLC V) +* (Af --> r) )

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

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;

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;

.= 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: verum

end;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

proof

then A12:
Af = Carrier Ar
by A3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Af or x in Carrier Ar )

assume A11: x in Af ; :: thesis: x in Carrier Ar

then Ar . x = (Af --> r) . x by A1, FUNCT_4:13;

hence x in Carrier Ar by A7, A11; :: thesis: verum

end;assume A11: x in Af ; :: thesis: x in Carrier Ar

then Ar . x = (Af --> r) . x by A1, FUNCT_4:13;

hence x in Carrier Ar by A7, A11; :: thesis: verum

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;

now :: thesis: for i being Nat st i in Seg (len F) holds

ArF . i = ((len F) |-> r) . i

then
ArF = (len F) |-> r
by FINSEQ_2:119;ArF . i = ((len F) |-> r) . i

let i be Nat; :: thesis: ( i in Seg (len F) implies ArF . i = ((len F) |-> r) . i )

assume A15: i in Seg (len F) ; :: thesis: ArF . i = ((len F) |-> r) . i

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: verum

end;assume A15: i in Seg (len F) ; :: thesis: ArF . i = ((len F) |-> r) . i

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: verum

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;

now :: thesis: for i being Nat st i in dom F holds

(Ar (#) F) . i = r * (F /. i)

then Sum Ar =
r * (Sum F)
by A10, A19, RLVECT_2:3
(Ar (#) F) . i = r * (F /. i)

let i be Nat; :: thesis: ( i in dom F implies (Ar (#) F) . i = r * (F /. i) )

assume A21: i in dom F ; :: thesis: (Ar (#) F) . i = r * (F /. i)

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: verum

end;assume A21: i in dom F ; :: thesis: (Ar (#) F) . i = r * (F /. i)

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: verum

.= 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: verum