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 real-valued FinSequence ;
thus (Mx2Tran M) . (p1 - p2) = (Mx2Tran M) . (f1 - f2) by EUCLID:69
.= ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2) by Th24
.= ((Mx2Tran M) . p1) - ((Mx2Tran M) . p2) by EUCLID:69 ; :: thesis: verum