let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real ex L being m -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
let M be Matrix of n,m,F_Real; :: thesis: ex L being m -element FinSequence of REAL st
( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
set F = the n -element real-valued FinSequence;
consider L being m -element FinSequence of REAL such that
|.((Mx2Tran M) . the n -element real-valued FinSequence).| <= (Sum L) * |. the n -element real-valued FinSequence.| and
A1: for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| by Lm4;
take L ; :: thesis: ( ( for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| ) & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| ) )
thus for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| by A1; :: thesis: for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.|
let f be n -element real-valued FinSequence; :: thesis: |.((Mx2Tran M) . f).| <= (Sum L) * |.f.|
consider L1 being m -element FinSequence of REAL such that
A2: |.((Mx2Tran M) . f).| <= (Sum L1) * |.f.| and
A3: for i being Nat st i in dom L1 holds
L1 . i = |.(@ (Col (M,i))).| by Lm4;
( len L1 = m & len L = m ) by CARD_1:def 7;
then A4: dom L = dom L1 by FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom L holds
L . i = L1 . i

let i be Nat; :: thesis: ( i in dom L implies L . i = L1 . i )
assume A5: i in dom L ; :: thesis: L . i = L1 . i
hence L . i = |.(@ (Col (M,i))).| by A1
.= L1 . i by A3, A4, A5 ;
:: thesis: verum

end;

hence |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| by A2, A4, FINSEQ_1:13; :: thesis: verum