theorem Th32: :: MIDSP_3:32

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 (a,x) . W = p & m <= n holds
(a,(x +* ((m + 1),(x . m)))) . W = p +* ((m + 1),(p . m))