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
for l being Nat of n st l = i holds
(p +* (i,d)) . l = d