theorem Th45: :: MATRTOP1:45

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