theorem Th25: :: MIDSP_3:25

for n being Nat
for m being Nat of n
for RAS being ReperAlgebra of n
for a, b being Point of RAS
for p being Tuple of (n + 1),RAS
for W being ATLAS of RAS
for v being Vector of W
for x being Tuple of (n + 1),W st W . (a,p) = x & W . (a,b) = v holds
W . (a,(p +* (m,b))) = x +* (m,v)