let m, n be non zero Element of NAT ; :: thesis: 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).||
let s, t be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))); :: thesis: 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).||
let si, ti be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); :: thesis: for i being Nat st si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n holds
||.(si - ti).|| <= ||.(s - t).||
let i be Nat; :: thesis: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n implies ||.(si - ti).|| <= ||.(s - t).|| )
deffunc H₁( Element of NAT , Element of NAT ) -> Element of K10(K11((BoundedLinearOperators ((REAL-NS $1),(REAL-NS $2))),REAL)) = BoundedLinearOperatorsNorm ((REAL-NS $1),(REAL-NS $2));
assume A1: ( si = (Proj (i,n)) * s & ti = (Proj (i,n)) * t & 1 <= i & i <= n ) ; :: thesis: ||.(si - ti).|| <= ||.(s - t).||
si - ti = (Proj (i,n)) * (s - t) by Lm1, A1;
hence ||.(si - ti).|| <= ||.(s - t).|| by A1, Th13; :: thesis: verum