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

now :: thesis: for i being Element of NAT
for sti being Point of H₁(m,1) st sti = (Proj (i,n)) * (s - t) & 1 <= i & i <= n holds
||.sti.|| <= K

let i be Element of NAT ; :: thesis: for sti being Point of H₁(m,1) st sti = (Proj (i,n)) * (s - t) & 1 <= i & i <= n holds
||.sti.|| <= K
let sti be Point of H₁(m,1); :: thesis: ( sti = (Proj (i,n)) * (s - t) & 1 <= i & i <= n implies ||.sti.|| <= K )
assume A2: ( sti = (Proj (i,n)) * (s - t) & 1 <= i & i <= n ) ; :: thesis: ||.sti.|| <= K
reconsider si = (Proj (i,n)) * s, ti = (Proj (i,n)) * t as Point of H₁(m,1) by Th7, A2;
si - ti = sti by A2, Lm1;
hence ||.sti.|| <= K by A2, A1; :: thesis: verum

end;

hence ||.(s - t).|| <= n * K by Th18; :: thesis: verum