theorem :: MIDSP_3:6

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