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 A1, RLAFFIN1:def 7;
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 RLAFFIN1:53, RLVECT_1:def 8;
( Carrier (v + (w |-- Affv)) = v + (Carrier (w |-- Affv)) & Carrier (w |-- Affv) c= Affv ) by RLAFFIN1:16, RLVECT_2:def 6;
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 A1, RLAFFIN1:def 7;
then A7: Sum vwA = (1 * v) + w by A3, RLAFFIN1:39;
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 A8, FINSEQ_3:29;
rng Ev = v + Affv by Def1;
then A11: len Ev = card Affv by A9, FINSEQ_4:62;
sum vwA = 1 by A3, RLAFFIN1:37;
then A12: vwA = (v + w) |-- (v + Affv) by A4, A7, A6, RLAFFIN1:def 7;

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 A8, A5, FINSEQ_3:29;
then A15: EV . i = EV /. i by A13, PARTFUN1:def 6;
i in Seg (card Affv) by A8, A13, FINSEQ_1:def 3;
then A16: cAv . i = v by FINSEQ_2:57;
A17: ((v + w) |-- Ev) . i = ((v + w) |-- (v + Affv)) . (Ev . i) by A10, A13, FUNCT_1:12;
dom Ev = dom (w |-- EV) by A8, A11, FINSEQ_3:29;
then Ev . i = (EV /. i) + v by A2, A13, A16, A15, FVSUM_1:17;
hence ((v + w) |-- Ev) . i = (w |-- Affv) . (((EV /. i) + v) - v) by A12, A17, RLAFFIN1:def 1
.= (w |-- Affv) . ((EV /. i) + (v - v)) by RLVECT_1:28
.= (w |-- Affv) . ((EV /. i) + (0. V)) by RLVECT_1:15
.= (w |-- EV) . i by A14, A15, RLVECT_1:def 4 ;
:: thesis: verum

end;

hence w |-- EV = (v + w) |-- Ev by A10, FINSEQ_1:13; :: thesis: verum