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;

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

hence
w |-- EV = (v + w) |-- Ev
by A10, FINSEQ_1:13; :: thesis: verum((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;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