let n, m be Nat; :: thesis: for M being Matrix of n,m,F_Real ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )
let M be Matrix of n,m,F_Real; :: thesis: ex L being Real st
( L > 0 & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= L * |.f.| ) )
consider L being m -element FinSequence of REAL such that
A1: for i being Nat st i in dom L holds
L . i = |.(@ (Col (M,i))).| and
A2: for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= (Sum L) * |.f.| by Th44;
reconsider S1 = 1 + (Sum L) as Real ;
take S1 ; :: thesis: ( S1 > 0 & ( for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= S1 * |.f.| ) )
now :: thesis: for i being Nat st i in dom L holds
0 <= L . i
let i be Nat; :: thesis: ( i in dom L implies 0 <= L . i )
assume i in dom L ; :: thesis: 0 <= L . i
then L . i = |.(@ (Col (M,i))).| by A1;
hence 0 <= L . i ; :: thesis: verum
end;
then Sum L >= 0 by RVSUM_1:84;
hence S1 > 0 ; :: thesis: for f being n -element real-valued FinSequence holds |.((Mx2Tran M) . f).| <= S1 * |.f.|
let f be n -element real-valued FinSequence; :: thesis: |.((Mx2Tran M) . f).| <= S1 * |.f.|
Sum L <= S1 by XREAL_1:29;
then A3: (Sum L) * |.f.| <= S1 * |.f.| by XREAL_1:64;
|.((Mx2Tran M) . f).| <= (Sum L) * |.f.| by A2;
hence |.((Mx2Tran M) . f).| <= S1 * |.f.| by A3, XXREAL_0:2; :: thesis: verum