let m be positive Nat; :: thesis: for j being Nat
for ks being Real st j in Seg m & 0 <= ks & ks <= m holds
|.(j - ks).| <= m
let j be Nat; :: thesis: for ks being Real st j in Seg m & 0 <= ks & ks <= m holds
|.(j - ks).| <= m
let ks be Real; :: thesis: ( j in Seg m & 0 <= ks & ks <= m implies |.(j - ks).| <= m )
assume A1: ( j in Seg m & 0 <= ks & ks <= m ) ; :: thesis: |.(j - ks).| <= m
reconsider jks = j - ks as Real ;
( j <= m & 0 <= ks ) by FINSEQ_1:1, A1;
then j + 0 <= m + ks by XREAL_1:7;
then A3: j - ks <= (m + ks) - ks by XREAL_1:9;
ks + 0 <= m + j by A1, XREAL_1:7;
then ks - j <= (m + j) - j by XREAL_1:9;
then (- 1) * m <= (- 1) * (ks - j) by XREAL_1:65;
then ( - m <= jks & jks <= m ) by A3;
hence |.(j - ks).| <= m by ABSVALUE:5; :: thesis: verum