theorem :: MIDSP_3:12

for n, i being Nat
for RAS being non empty MidSp-like ReperAlgebraStr over n + 2
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st i in Seg (n + 1) holds
( (x +* (i,v)) . i = v & ( for l being Nat st l in (dom x) \ {i} holds
(x +* (i,v)) . l = x . l ) ) by Lm1, Lm2;