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;

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

hence
v |-- EV = (r * v) |-- rE
by A12, FINSEQ_1:13; :: thesis: verum((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;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