deffunc H₁( non zero Nat, non zero Nat) -> L16() = R_NormSpace_of_BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2));
let m, n be non zero Element of NAT ; :: thesis: for s being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
let s be Point of H₁(m,n); :: thesis: for K being Real st ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
||.s.|| <= n * K
let K be Real; :: thesis: ( ( for i being Element of NAT
for si being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) implies ||.s.|| <= n * K )
assume A1: for i being Element of NAT
for si being Point of H₁(m,1) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ; :: thesis: ||.s.|| <= n * K
reconsider s0 = s as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;

A2: now :: thesis: for x being Point of (REAL-NS m) st ||.x.|| <= 1 holds
||.(s0 . x).|| <= n * K

let x be Point of (REAL-NS m); :: thesis: ( ||.x.|| <= 1 implies ||.(s0 . x).|| <= n * K )
assume A3: ||.x.|| <= 1 ; :: thesis: ||.(s0 . x).|| <= n * K

now :: thesis: for i being Element of NAT st 1 <= i & i <= n holds
||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.|| )
assume A4: ( 1 <= i & i <= n ) ; :: thesis: ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.||
set si = (Proj (i,n)) * s;
reconsider si = (Proj (i,n)) * s as Point of H₁(m,1) by Th7, A4;
reconsider sii = si as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS 1) by LOPBAN_1:def 9;
A5: ||.(sii . x).|| <= ||.si.|| * ||.x.|| by LOPBAN_1:32;
A6: the carrier of (REAL-NS m) = REAL m by REAL_NS1:def 4;
A7: Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) by A4, Th6;
s is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;
then (Proj (i,n)) * s is LinearOperator of (REAL-NS m),(REAL-NS 1) by A7, LOPBAN_2:1;
then dom ((Proj (i,n)) * s) = REAL m by A6, FUNCT_2:def 1;
then A8: sii . x = (Proj (i,n)) . (s . x) by A6, FUNCT_1:12;
A9: 0 <= ||.x.|| by NORMSP_1:4;
||.si.|| * ||.x.|| <= K * ||.x.|| by A4, A1, A9, XREAL_1:64;
hence ||.((Proj (i,n)) . (s . x)).|| <= K * ||.x.|| by A5, A8, XXREAL_0:2; :: thesis: verum

end;

then A10: ||.(s . x).|| <= n * (K * ||.x.||) by Th16;
A11: ( 1 <= 1 & 1 <= n ) by NAT_1:14;
then reconsider s1 = (Proj (1,n)) * s as Point of H₁(m,1) by Th7;
||.s1.|| <= K by A11, A1;
then A12: 0 <= K by NORMSP_1:4;
(n * K) * ||.x.|| <= (n * K) * 1 by A12, A3, XREAL_1:64;
hence ||.(s0 . x).|| <= n * K by A10, XXREAL_0:2; :: thesis: verum

end;

set PreNormS = PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)));
A13: for y being ExtReal st y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) holds
y <= n * K

proof

let y be ExtReal; :: thesis: ( y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) implies y <= n * K )
assume A14: y in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) ; :: thesis: y <= n * K
consider x being VECTOR of (REAL-NS m) such that
A15: ( y = ||.((modetrans (s,(REAL-NS m),(REAL-NS n))) . x).|| & ||.x.|| <= 1 ) by A14;
y = ||.(s0 . x).|| by A15, LOPBAN_1:29;
hence y <= n * K by A2, A15; :: thesis: verum

end;

A16: PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above

proof

n * K is UpperBound of PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) by A13, XXREAL_2:def 1;
hence PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) is bounded_above by XXREAL_2:def 10; :: thesis: verum

end;

set UBPreNormS = upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))));
not upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K

proof

assume A17: upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n)))) > n * K ; :: thesis: contradiction
set dif = (upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K);
A18: (upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K) > 0 by A17, XREAL_1:50;
consider w being Real such that
A19: ( w in PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))) & (upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - ((upper_bound (PreNorms (modetrans (s,(REAL-NS m),(REAL-NS n))))) - (n * K)) < w ) by A18, A16, SEQ_4:def 1;
thus contradiction by A19, A13; :: thesis: verum

end;

then upper_bound (PreNorms s0) <= n * K by LOPBAN_1:def 11;
hence ||.s.|| <= n * K by LOPBAN_1:30; :: thesis: verum