theorem Th44: :: MATRTOP1:44

for n, m being Nat
for M being Matrix of n,m,F_Real ex L being b₂ -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being b₁ -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )