deffunc H1( 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 ()
for K being Real st ( for i being Element of NAT
for si being Point of () st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
<= n * K

let s be Point of H1(m,n); :: thesis: for K being Real st ( for i being Element of NAT
for si being Point of () st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) holds
<= n * K

let K be Real; :: thesis: ( ( for i being Element of NAT
for si being Point of () st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ) implies <= n * K )

assume A1: for i being Element of NAT
for si being Point of H1(m,1) st si = (Proj (i,n)) * s & 1 <= i & i <= n holds
||.si.|| <= K ; :: thesis: <= n * K
reconsider s0 = s as Lipschitzian LinearOperator of (),() by LOPBAN_1:def 9;
A2: now :: thesis: for x being Point of () st <= 1 holds
||.(s0 . x).|| <= n * K
let x be Point of (); :: thesis: ( <= 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 *
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= n implies ||.((Proj (i,n)) . (s . x)).|| <= K * )
assume A4: ( 1 <= i & i <= n ) ; :: thesis: ||.((Proj (i,n)) . (s . x)).|| <= K *
set si = (Proj (i,n)) * s;
reconsider si = (Proj (i,n)) * s as Point of H1(m,1) by ;
reconsider sii = si as Lipschitzian LinearOperator of (),() by LOPBAN_1:def 9;
A5: ||.(sii . x).|| <= ||.si.|| * by LOPBAN_1:32;
A6: the carrier of () = REAL m by REAL_NS1:def 4;
A7: Proj (i,n) is Lipschitzian LinearOperator of (),() by ;
s is Lipschitzian LinearOperator of (),() by LOPBAN_1:def 9;
then (Proj (i,n)) * s is LinearOperator of (),() by ;
then dom ((Proj (i,n)) * s) = REAL m by ;
then A8: sii . x = (Proj (i,n)) . (s . x) by ;
A9: 0 <= by NORMSP_1:4;
||.si.|| * <= K * by ;
hence ||.((Proj (i,n)) . (s . x)).|| <= K * by ; :: thesis: verum
end;
then A10: ||.(s . x).|| <= n * (K * ) by Th16;
A11: ( 1 <= 1 & 1 <= n ) by NAT_1:14;
then reconsider s1 = (Proj (1,n)) * s as Point of H1(m,1) by Th7;
||.s1.|| <= K by ;
then A12: 0 <= K by NORMSP_1:4;
(n * K) * <= (n * K) * 1 by ;
hence ||.(s0 . x).|| <= n * K by ; :: thesis: verum
end;
set PreNormS = PreNorms (modetrans (s,(),()));
A13: for y being ExtReal st y in PreNorms (modetrans (s,(),())) holds
y <= n * K
proof
let y be ExtReal; :: thesis: ( y in PreNorms (modetrans (s,(),())) implies y <= n * K )
assume A14: y in PreNorms (modetrans (s,(),())) ; :: thesis: y <= n * K
consider x being VECTOR of () such that
A15: ( y = ||.((modetrans (s,(),())) . x).|| & <= 1 ) by A14;
y = ||.(s0 . x).|| by ;
hence y <= n * K by ; :: thesis: verum
end;
A16: PreNorms (modetrans (s,(),())) is bounded_above
proof
n * K is UpperBound of PreNorms (modetrans (s,(),())) by ;
hence PreNorms (modetrans (s,(),())) is bounded_above by XXREAL_2:def 10; :: thesis: verum
end;
set UBPreNormS = upper_bound (PreNorms (modetrans (s,(),())));
not upper_bound (PreNorms (modetrans (s,(),()))) > n * K
proof
assume A17: upper_bound (PreNorms (modetrans (s,(),()))) > n * K ; :: thesis: contradiction
set dif = (upper_bound (PreNorms (modetrans (s,(),())))) - (n * K);
A18: (upper_bound (PreNorms (modetrans (s,(),())))) - (n * K) > 0 by ;
consider w being Real such that
A19: ( w in PreNorms (modetrans (s,(),())) & (upper_bound (PreNorms (modetrans (s,(),())))) - ((upper_bound (PreNorms (modetrans (s,(),())))) - (n * K)) < w ) by ;
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