let n, m be Nat; :: thesis: for f1, f2 being n -element real-valued FinSequence
for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
let f1, f2 be n -element real-valued FinSequence; :: thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
let M be Matrix of n,m,F_Real; :: thesis: (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2)
f1 - f2 = f1 + (- f2) by RVSUM_1:31
.= f1 + ((- 1) * f2) by RVSUM_1:54 ;
hence (Mx2Tran M) . (f1 - f2) = ((Mx2Tran M) . f1) + ((Mx2Tran M) . ((- 1) * f2)) by Th22
.= ((Mx2Tran M) . f1) + ((- 1) * ((Mx2Tran M) . f2)) by Th23
.= ((Mx2Tran M) . f1) + (- ((Mx2Tran M) . f2)) by RVSUM_1:54
.= ((Mx2Tran M) . f1) - ((Mx2Tran M) . f2) by RVSUM_1:31 ;
:: thesis: verum