let f1, f2 be Point of (TOP-REAL n); :: according to GRCAT_1:def 8 :: thesis: (Mx2Tran A) . (f1 + f2) = ((Mx2Tran A) . f1) + ((Mx2Tran A) . f2)
thus (Mx2Tran A) . (f1 + f2) = ((Mx2Tran A) . f1) + ((Mx2Tran A) . f2) by MATRTOP1:22; :: thesis: verum