theorem :: MATRTOP1:38

for n, m being Nat
for f being b₁ -element real-valued FinSequence
for M being Matrix of n,m,F_Real st M = (1. (F_Real,m)) | n holds
((Mx2Tran M) . f) | n = f