theorem Th13: :: MIDSP_3:13

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