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 i being 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.|| <= ||.s.||
let s be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); :: thesis: for i being 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.|| <= ||.s.||
let i be Nat; :: thesis: 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.|| <= ||.s.||
let si be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); :: thesis: ( si = (Proj (i,n)) * s & 1 <= i & i <= n implies ||.si.|| <= ||.s.|| )
assume A1: ( si = (Proj (i,n)) * s & 1 <= i & i <= n ) ; :: thesis: ||.si.|| <= ||.s.||
deffunc H₁( Nat, Nat) -> Element of K10(K11((BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2))),REAL)) = BoundedLinearOperatorsNorm ((REAL-NS $1),(REAL-NS $2));
A2: ( Proj (i,n) is Lipschitzian LinearOperator of (REAL-NS n),(REAL-NS 1) & H₁(n,1) . (Proj (i,n)) <= 1 ) by Th6, A1;
s is Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;
then A3: ||.si.|| <= (H₁(n,1) . (Proj (i,n))) * ||.s.|| by A2, A1, LOPBAN_2:2;
0 <= ||.s.|| by NORMSP_1:4;
then (H₁(n,1) . (Proj (i,n))) * ||.s.|| <= 1 * ||.s.|| by Th6, A1, XREAL_1:64;
hence ||.si.|| <= ||.s.|| by A3, XXREAL_0:2; :: thesis: verum