let n, m be Nat; :: thesis: 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)
let p1, p2 be Point of (TOP-REAL n); :: thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (p1 + p2) = ((Mx2Tran M) . p1) + ((Mx2Tran M) . p2)
let M be Matrix of n,m,F_Real; :: thesis: (Mx2Tran M) . (p1 + p2) = ((Mx2Tran M) . p1) + ((Mx2Tran M) . p2)
reconsider f1 = p1, f2 = p2 as n -element real-valued FinSequence ;
thus (Mx2Tran M) . (p1 + p2) = (Mx2Tran M) . (f1 + f2) by EUCLID:64
.= ((Mx2Tran M) . f1) + ((Mx2Tran M) . f2) by Th22
.= ((Mx2Tran M) . p1) + ((Mx2Tran M) . p2) by EUCLID:64 ; :: thesis: verum