theorem :: MATRTOP1:46

for n, m being Nat
for M being Matrix of n,m,F_Real st the_rank_of M = n holds
ex L being Real st
( L > 0 & ( for f being b₁ -element real-valued FinSequence holds |.f.| <= L * |.((Mx2Tran M) . f).| ) )