let V be RealLinearSpace; :: thesis: for v, w being VECTOR of V
for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E

let v, w be VECTOR of V; :: thesis: for Affv being finite affinely-independent Subset of V
for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E

let Affv be finite affinely-independent Subset of V; :: thesis: for EV being Enumeration of Affv
for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E

let EV be Enumeration of Affv; :: thesis: for E being Enumeration of v + Affv st w in Affin Affv & E = EV + ((card Affv) |-> v) holds
w |-- EV = (v + w) |-- E

set E = EV;
let Ev be Enumeration of v + Affv; :: thesis: ( w in Affin Affv & Ev = EV + ((card Affv) |-> v) implies w |-- EV = (v + w) |-- Ev )
assume that
A1: w in Affin Affv and
A2: Ev = EV + ((card Affv) |-> v) ; :: thesis: w |-- EV = (v + w) |-- Ev
set wA = w |-- Affv;
A3: sum (w |-- Affv) = 1 by ;
v + w in { (v + u) where u is VECTOR of V : u in Affin Affv } by A1;
then A4: v + w in v + (Affin Affv) by RUSUB_4:def 8;
rng EV = Affv by Def1;
then A5: len EV = card Affv by FINSEQ_4:62;
then reconsider e = EV, cAv = (card Affv) |-> v as Element of (card Affv) -tuples_on the carrier of V by FINSEQ_2:92;
A6: ( Affin (v + Affv) = v + (Affin Affv) & 1 * v = v ) by ;
( Carrier (v + (w |-- Affv)) = v + (Carrier (w |-- Affv)) & Carrier (w |-- Affv) c= Affv ) by ;
then Carrier (v + (w |-- Affv)) c= v + Affv by RLTOPSP1:8;
then reconsider vwA = v + (w |-- Affv) as Linear_Combination of v + Affv by RLVECT_2:def 6;
Sum (w |-- Affv) = w by ;
then A7: Sum vwA = (1 * v) + w by ;
A8: len (w |-- EV) = card Affv by Th16;
A9: card Affv = card (v + Affv) by RLAFFIN1:7;
then len ((v + w) |-- Ev) = card Affv by Th16;
then A10: dom (w |-- EV) = dom ((v + w) |-- Ev) by ;
rng Ev = v + Affv by Def1;
then A11: len Ev = card Affv by ;
sum vwA = 1 by ;
then A12: vwA = (v + w) |-- (v + Affv) by ;
now :: thesis: for i being Nat st i in dom (w |-- EV) holds
((v + w) |-- Ev) . i = (w |-- EV) . i
let i be Nat; :: thesis: ( i in dom (w |-- EV) implies ((v + w) |-- Ev) . i = (w |-- EV) . i )
assume A13: i in dom (w |-- EV) ; :: thesis: ((v + w) |-- Ev) . i = (w |-- EV) . i
then A14: (w |-- EV) . i = (w |-- Affv) . (EV . i) by FUNCT_1:12;
dom EV = dom (w |-- EV) by ;
then A15: EV . i = EV /. i by ;
i in Seg (card Affv) by ;
then A16: cAv . i = v by FINSEQ_2:57;
A17: ((v + w) |-- Ev) . i = ((v + w) |-- (v + Affv)) . (Ev . i) by ;
dom Ev = dom (w |-- EV) by ;
then Ev . i = (EV /. i) + v by ;
hence ((v + w) |-- Ev) . i = (w |-- Affv) . (((EV /. i) + v) - v) by
.= (w |-- Affv) . ((EV /. i) + (v - v)) by RLVECT_1:28
.= (w |-- Affv) . ((EV /. i) + (0. V)) by RLVECT_1:15
.= (w |-- EV) . i by ;
:: thesis: verum
end;
hence w |-- EV = (v + w) |-- Ev by ; :: thesis: verum