theorem Th14: :: PDIFF_8:14

for m, n being non zero Element of NAT
for s, t being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
for si, ti being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1)))
for i being Nat st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= ||.(s - t).||