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 ;
Carrier (r (*) (v |-- Affv)) = r * (Carrier (v |-- Affv)) by ;
then Carrier (r (*) (v |-- Affv)) c= r * Affv by ;
then reconsider rvA = r (*) (v |-- Affv) as Linear_Combination of r * Affv by RLVECT_2:def 6;
sum (v |-- Affv) = 1 by ;
then A7: sum rvA = 1 by ;
Sum (v |-- Affv) = v by ;
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 ;
card Affv = card (r * Affv) by ;
then A12: dom (v |-- EV) = dom ((r * v) |-- rE) by ;
Affin (r * Affv) = r * (Affin Affv) by ;
then r * v in Affin (r * Affv) by ;
then A13: rvA = (r * v) |-- (r * Affv) by ;
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 ;
A16: rE /. k = r * (EV /. k) by ;
( ((r * v) |-- rE) . k = rvA . (rE . k) & rE /. k = rE . k ) by ;
hence ((r * v) |-- rE) . k = (v |-- Affv) . ((r ") * (r * (EV /. k))) by
.= (v |-- Affv) . (((r ") * r) * (EV /. k)) by RLVECT_1:def 7
.= (v |-- Affv) . (1 * (EV /. k)) by
.= (v |-- EV) . k by ;
:: thesis: verum
end;
hence v |-- EV = (r * v) |-- rE by ; :: thesis: verum