theorem Th28: :: MATRTOP1:28

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 Th24;