theorem Th31: :: MIDSP_3:31

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