let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real holds (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
let M be Matrix of n,m,F_Real; :: thesis: (Mx2Tran M) . (0. (TOP-REAL n)) = 0. (TOP-REAL m)
set TRn = the Element of (TOP-REAL n);
set MT = Mx2Tran M;
0. (TOP-REAL n) = the Element of (TOP-REAL n) - the Element of (TOP-REAL n) by RLVECT_1:5;
hence (Mx2Tran M) . (0. (TOP-REAL n)) = ((Mx2Tran M) . the Element of (TOP-REAL n)) - ((Mx2Tran M) . the Element of (TOP-REAL n)) by Th28
.= 0. (TOP-REAL m) by RLVECT_1:5 ;
:: thesis: verum