theorem Th27: :: MATRTOP1:27

for n, m being Nat
for p1, p2 being Point of (TOP-REAL n)
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (p1 + p2) = ((Mx2Tran M) . p1) + ((Mx2Tran M) . p2) by Th22;