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