theorem Th7: :: PDIFF_8:7

for m, n being non zero Element of NAT
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) )