let r be Real; :: thesis: for V being RealLinearSpace
for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let v be VECTOR of V; :: thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let Affv be finite affinely-independent Subset of V; :: thesis: for EV being Enumeration of Affv
for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
let EV be Enumeration of Affv; :: thesis: for rE being Enumeration of r * Affv st v in Affin Affv & rE = r (#) EV & r <> 0 holds
v |-- EV = (r * v) |-- rE
set E = EV;
let rE be Enumeration of r * Affv; :: thesis: ( v in Affin Affv & rE = r (#) EV & r <> 0 implies v |-- EV = (r * v) |-- rE )
assume that
A1: v in Affin Affv and
A2: rE = r (#) EV and
A3: r <> 0 ; :: thesis: v |-- EV = (r * v) |-- rE
set vA = v |-- Affv;
A4: Carrier (v |-- Affv) c= Affv by RLVECT_2:def 6;
A5: r * v in { (r * u) where u is VECTOR of V : u in Affin Affv } by A1;
A6: dom rE = dom EV by A2, VFUNCT_1:def 4;
Carrier (r (*) (v |-- Affv)) = r * (Carrier (v |-- Affv)) by A3, RLAFFIN1:23;
then Carrier (r (*) (v |-- Affv)) c= r * Affv by A4, CONVEX1:39;
then reconsider rvA = r (*) (v |-- Affv) as Linear_Combination of r * Affv by RLVECT_2:def 6;
sum (v |-- Affv) = 1 by A1, RLAFFIN1:def 7;
then A7: sum rvA = 1 by A3, RLAFFIN1:38;
Sum (v |-- Affv) = v by A1, RLAFFIN1:def 7;
then A8: Sum rvA = r * v by RLAFFIN1:40;
A9: len ((r * v) |-- rE) = card (r * Affv) by Th16;
A10: len (v |-- EV) = card Affv by Th16;
rng EV = Affv by Def1;
then len EV = card Affv by FINSEQ_4:62;
then A11: dom (v |-- EV) = dom EV by A10, FINSEQ_3:29;
card Affv = card (r * Affv) by A3, Th12;
then A12: dom (v |-- EV) = dom ((r * v) |-- rE) by A10, A9, FINSEQ_3:29;
Affin (r * Affv) = r * (Affin Affv) by A3, RLAFFIN1:55;
then r * v in Affin (r * Affv) by A5, CONVEX1:def 1;
then A13: rvA = (r * v) |-- (r * Affv) by A7, A8, RLAFFIN1:def 7;

now :: thesis: for k being Nat st k in dom (v |-- EV) holds
((r * v) |-- rE) . k = (v |-- EV) . k

let k be Nat; :: thesis: ( k in dom (v |-- EV) implies ((r * v) |-- rE) . k = (v |-- EV) . k )
assume A14: k in dom (v |-- EV) ; :: thesis: ((r * v) |-- rE) . k = (v |-- EV) . k
then A15: ( (v |-- EV) . k = (v |-- Affv) . (EV . k) & EV /. k = EV . k ) by A11, FUNCT_1:12, PARTFUN1:def 6;
A16: rE /. k = r * (EV /. k) by A2, A11, A6, A14, VFUNCT_1:def 4;
( ((r * v) |-- rE) . k = rvA . (rE . k) & rE /. k = rE . k ) by A13, A12, A11, A6, A14, FUNCT_1:12, PARTFUN1:def 6;
hence ((r * v) |-- rE) . k = (v |-- Affv) . ((r ") * (r * (EV /. k))) by A3, A16, RLAFFIN1:def 2
.= (v |-- Affv) . (((r ") * r) * (EV /. k)) by RLVECT_1:def 7
.= (v |-- Affv) . (1 * (EV /. k)) by A3, XCMPLX_0:def 7
.= (v |-- EV) . k by A15, RLVECT_1:def 8 ;
:: thesis: verum

end;

hence v |-- EV = (r * v) |-- rE by A12, FINSEQ_1:13; :: thesis: verum