let n be non zero Nat; :: thesis: for jn, j, k being Nat
for p being Element of (FTSL1 n) st p = jn holds
( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) )
let jn, j, k be Nat; :: thesis: for p being Element of (FTSL1 n) st p = jn holds
( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) )
let p be Element of (FTSL1 n); :: thesis: ( p = jn implies ( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) ) )
A1: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;
assume A2: p = jn ; :: thesis: ( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) )

A3: now :: thesis: ( j in Seg n & |.(jn - j).| <= k + 1 implies j in U_FT (p,k) )

defpred S₁[ Nat] means for j2, jn2 being Nat
for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in Seg n & |.(jn2 - j2).| <= $1 + 1 holds
j2 in U_FT (p2,$1);
A4: S₁[ 0 ]

proof

let j2, jn2 be Nat; :: thesis: for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in Seg n & |.(jn2 - j2).| <= 0 + 1 holds
j2 in U_FT (p2,0)
let p2 be Element of (FTSL1 n); :: thesis: ( jn2 = p2 & j2 in Seg n & |.(jn2 - j2).| <= 0 + 1 implies j2 in U_FT (p2,0) )
assume that
A5: jn2 = p2 and
A6: j2 in Seg n and
A7: |.(jn2 - j2).| <= 0 + 1 ; :: thesis: j2 in U_FT (p2,0)
A8: j2 <= n by A6, FINSEQ_1:1;
A9: 1 <= j2 by A6, FINSEQ_1:1;

now :: thesis: ( ( jn2 - j2 >= 0 & ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) ) or ( jn2 - j2 < 0 & ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) ) )

per cases ( jn2 - j2 >= 0 or jn2 - j2 < 0 ) ;

case jn2 - j2 >= 0 ; :: thesis: verum

then A10: jn2 - j2 = jn2 -' j2 by XREAL_0:def 2;
A11: ( jn2 -' j2 >= 0 + 1 or jn2 -' j2 = 0 ) by NAT_1:13;
jn2 - j2 <= 1 by A7, ABSVALUE:def 1;
then A12: ( jn2 - j2 = 1 or jn2 -' j2 = 0 ) by A10, A11, XXREAL_0:1;

per cases ( jn2 - 1 = j2 or jn2 = j2 ) by A10, A12;

suppose A13: jn2 - 1 = j2 ; :: thesis: ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) )

then jn2 - 1 = jn2 -' 1 by XREAL_0:def 2;
hence ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) by A9, A13, XXREAL_0:def 10; :: thesis: verum

end;

suppose jn2 = j2 ; :: thesis: ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) )

hence ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) ; :: thesis: verum

end;

end;

end;

case A14: jn2 - j2 < 0 ; :: thesis: ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) )

then (jn2 - j2) + j2 < 0 + j2 by XREAL_1:8;
then A15: jn2 + 1 <= j2 by NAT_1:13;
- (jn2 - j2) <= 1 by A7, A14, ABSVALUE:def 1;
then (j2 - jn2) + jn2 <= 1 + jn2 by XREAL_1:7;
then jn2 + 1 = j2 by A15, XXREAL_0:1;
hence ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) by A8, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

then ( jn2 in NAT & j2 in {jn2,(max ((jn2 -' 1),1)),(min ((jn2 + 1),n))} ) by ENUMSET1:def 1, ORDINAL1:def 12;
then j2 in U_FT p2 by A1, A5, FINTOPO4:def 3;
hence j2 in U_FT (p2,0) by FINTOPO3:47; :: thesis: verum

end;

A16: for jj being Nat st S₁[jj] holds
S₁[jj + 1]

proof

let jj be Nat; :: thesis: ( S₁[jj] implies S₁[jj + 1] )
assume A17: S₁[jj] ; :: thesis: S₁[jj + 1]
let j2, jn2 be Nat; :: thesis: for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in Seg n & |.(jn2 - j2).| <= (jj + 1) + 1 holds
j2 in U_FT (p2,(jj + 1))
let p2 be Element of (FTSL1 n); :: thesis: ( jn2 = p2 & j2 in Seg n & |.(jn2 - j2).| <= (jj + 1) + 1 implies j2 in U_FT (p2,(jj + 1)) )
assume that
A18: jn2 = p2 and
A19: j2 in Seg n and
A20: |.(jn2 - j2).| <= (jj + 1) + 1 ; :: thesis: j2 in U_FT (p2,(jj + 1))
A21: j2 <= n by A19, FINSEQ_1:1;
reconsider x0 = j2 as Element of (FTSL1 n) by A1, A19;
A22: 1 <= j2 by A19, FINSEQ_1:1;
A23: jn2 <= n by A1, A18, FINSEQ_1:1;
A24: 1 <= jn2 by A1, A18, FINSEQ_1:1;

A25: now :: thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )

per cases ( jn2 - j2 >= 0 or jn2 - j2 < 0 ) ;

suppose A26: jn2 - j2 >= 0 ; :: thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )

per cases ( jn2 - j2 = 0 or jn2 - j2 > 0 ) by A26;

suppose A27: jn2 - j2 = 0 ; :: thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )

FTSL1 n is filled by FINTOPO4:18;
then A28: x0 in U_FT p2 by A18, A27;
|.(jn2 - j2).| <= jj + 1 by A27, ABSVALUE:def 1;
hence ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y ) by A17, A18, A19, A27, A28; :: thesis: verum

end;

suppose A29: jn2 - j2 > 0 ; :: thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )

then jn2 - j2 = jn2 -' j2 by XREAL_0:def 2;
then A30: jn2 - j2 >= 0 + 1 by A29, NAT_1:13;
then (jn2 - j2) + j2 >= 1 + j2 by XREAL_1:7;
then A31: n >= j2 + 1 by A23, XXREAL_0:2;
j2 < j2 + 1 by NAT_1:13;
then A32: jn2 - (j2 + 1) < jn2 - j2 by XREAL_1:15;
|.(jn2 - j2).| = jn2 - j2 by A29, ABSVALUE:def 1;
then A33: jn2 - (j2 + 1) < (jj + 1) + 1 by A20, A32, XXREAL_0:2;
A34: (jn2 - j2) - 1 >= 1 - 1 by A30, XREAL_1:9;
then jn2 -' (j2 + 1) = jn2 - (j2 + 1) by XREAL_0:def 2;
then jn2 - (j2 + 1) <= jj + 1 by A33, NAT_1:13;
then A35: |.(jn2 - (j2 + 1)).| <= jj + 1 by A34, ABSVALUE:def 1;
1 <= j2 + 1 by A22, NAT_1:13;
then A36: j2 + 1 in Seg n by A31;
then reconsider yj2 = j2 + 1 as Element of (FTSL1 n) by A1;
|.((j2 + 1) - j2).| = 1 by ABSVALUE:def 1;
then x0 in U_FT (yj2,0) by A4, A19;
then x0 in U_FT yj2 by FINTOPO3:47;
hence ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y ) by A17, A18, A36, A35; :: thesis: verum

end;

end;

end;

suppose jn2 - j2 < 0 ; :: thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )

then A37: (jn2 - j2) + j2 < 0 + j2 by XREAL_1:6;
then A38: j2 - jn2 > 0 by XREAL_1:50;
j2 - 1 >= 0 by A22, XREAL_1:48;
then A39: j2 - 1 = j2 -' 1 by XREAL_0:def 2;
jn2 + 1 <= j2 by A37, NAT_1:13;
then A40: (jn2 + 1) - 1 <= j2 - 1 by XREAL_1:9;
then (j2 - 1) - jn2 >= 0 by XREAL_1:48;
then A41: |.((j2 -' 1) - jn2).| = (j2 -' 1) - jn2 by A39, ABSVALUE:def 1;
j2 < j2 + 1 by NAT_1:13;
then j2 - 1 < (j2 + 1) - 1 by XREAL_1:9;
then A42: j2 -' 1 < n by A21, A39, XXREAL_0:2;
|.(jn2 - j2).| = |.(j2 - jn2).| by UNIFORM1:11
.= 1 + ((j2 -' 1) - jn2) by A39, A38, ABSVALUE:def 1
.= 1 + |.(jn2 - (j2 -' 1)).| by A41, UNIFORM1:11 ;
then A43: |.(jn2 - (j2 -' 1)).| <= jj + 1 by A20, XREAL_1:6;
j2 -' 1 >= 1 by A24, A40, A39, XXREAL_0:2;
then A44: j2 -' 1 in Seg n by A42;
then reconsider pj21 = j2 -' 1 as Element of (FTSL1 n) by A1;
|.((j2 -' 1) - j2).| = |.(j2 - (j2 -' 1)).| by UNIFORM1:11
.= 1 by A39, ABSVALUE:def 1 ;
then x0 in U_FT (pj21,0) by A4, A19;
then x0 in U_FT pj21 by FINTOPO3:47;
hence ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y ) by A17, A18, A44, A43; :: thesis: verum

end;

end;

end;

U_FT (p2,(jj + 1)) = (U_FT (p2,jj)) ^f by FINTOPO3:48
.= { x where x is Element of (FTSL1 n) : ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x in U_FT y ) } ;
hence j2 in U_FT (p2,(jj + 1)) by A25; :: thesis: verum

end;

A45: for ii being Nat holds S₁[ii] from NAT_1:sch 2(A4, A16);
assume ( j in Seg n & |.(jn - j).| <= k + 1 ) ; :: thesis: j in U_FT (p,k)
hence j in U_FT (p,k) by A2, A45; :: thesis: verum

end;

now :: thesis: ( j in U_FT (p,k) implies ( j in Seg n & |.(jn - j).| <= k + 1 ) )

defpred S₁[ Nat] means for j2, jn2 being Nat
for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in U_FT (p2,$1) holds
|.(jn2 - j2).| <= $1 + 1;
A46: S₁[ 0 ]

proof

let j2, jn2 be Nat; :: thesis: for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in U_FT (p2,0) holds
|.(jn2 - j2).| <= 0 + 1
let p2 be Element of (FTSL1 n); :: thesis: ( jn2 = p2 & j2 in U_FT (p2,0) implies |.(jn2 - j2).| <= 0 + 1 )
assume that
A47: jn2 = p2 and
A48: j2 in U_FT (p2,0) ; :: thesis: |.(jn2 - j2).| <= 0 + 1
A49: j2 in U_FT p2 by A48, FINTOPO3:47;
jn2 in NAT by ORDINAL1:def 12;
then A50: Im ((Nbdl1 n),jn2) = {jn2,(max ((jn2 -' 1),1)),(min ((jn2 + 1),n))} by A1, A47, FINTOPO4:def 3;
A51: jn2 <= n by A1, A47, FINSEQ_1:1;

per cases ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) by A1, A47, A49, A50, ENUMSET1:def 1;

suppose j2 = jn2 ; :: thesis: |.(jn2 - j2).| <= 0 + 1

hence |.(jn2 - j2).| <= 0 + 1 by ABSVALUE:2; :: thesis: verum

end;

suppose A52: j2 = max ((jn2 -' 1),1) ; :: thesis: |.(jn2 - j2).| <= 0 + 1

per cases ( jn2 -' 1 >= 1 or jn2 -' 1 < 1 ) ;

suppose A53: jn2 -' 1 >= 1 ; :: thesis: |.(jn2 - j2).| <= 0 + 1

then j2 = jn2 -' 1 by A52, XXREAL_0:def 10;
then j2 = jn2 - 1 by A53, NAT_D:39;
hence |.(jn2 - j2).| <= 0 + 1 by ABSVALUE:def 1; :: thesis: verum

end;

suppose A54: jn2 -' 1 < 1 ; :: thesis: |.(jn2 - j2).| <= 0 + 1

then jn2 -' 1 < 0 + 1 ;
then jn2 -' 1 = 0 by NAT_1:13;
then A55: 1 - jn2 >= 0 by NAT_D:36, XREAL_1:48;
1 <= 1 + jn2 by NAT_1:12;
then A56: 1 - jn2 <= (1 + jn2) - jn2 by XREAL_1:9;
j2 = 1 by A52, A54, XXREAL_0:def 10;
then |.(j2 - jn2).| = 1 - jn2 by A55, ABSVALUE:def 1;
hence |.(jn2 - j2).| <= 0 + 1 by A56, UNIFORM1:11; :: thesis: verum

end;

end;

end;

suppose A57: j2 = min ((jn2 + 1),n) ; :: thesis: |.(jn2 - j2).| <= 0 + 1

per cases ( jn2 + 1 <= n or jn2 + 1 > n ) ;

suppose jn2 + 1 <= n ; :: thesis: |.(jn2 - j2).| <= 0 + 1

then j2 = jn2 + 1 by A57, XXREAL_0:def 9;
then |.(j2 - jn2).| = 1 by ABSVALUE:def 1;
hence |.(jn2 - j2).| <= 0 + 1 by UNIFORM1:11; :: thesis: verum

end;

suppose A58: jn2 + 1 > n ; :: thesis: |.(jn2 - j2).| <= 0 + 1

then jn2 >= n by NAT_1:13;
then A59: jn2 = n by A51, XXREAL_0:1;
j2 = n by A57, A58, XXREAL_0:def 9;
hence |.(jn2 - j2).| <= 0 + 1 by A59, ABSVALUE:2; :: thesis: verum

end;

end;

end;

end;

end;

A60: for i2 being Nat st S₁[i2] holds
S₁[i2 + 1]

proof

let i2 be Nat; :: thesis: ( S₁[i2] implies S₁[i2 + 1] )
assume A61: S₁[i2] ; :: thesis: S₁[i2 + 1]
let j3, jn3 be Nat; :: thesis: for p2 being Element of (FTSL1 n) st jn3 = p2 & j3 in U_FT (p2,(i2 + 1)) holds
|.(jn3 - j3).| <= (i2 + 1) + 1
let p2 be Element of (FTSL1 n); :: thesis: ( jn3 = p2 & j3 in U_FT (p2,(i2 + 1)) implies |.(jn3 - j3).| <= (i2 + 1) + 1 )
assume that
A62: jn3 = p2 and
A63: j3 in U_FT (p2,(i2 + 1)) ; :: thesis: |.(jn3 - j3).| <= (i2 + 1) + 1
U_FT (p2,(i2 + 1)) = (U_FT (p2,i2)) ^f by FINTOPO3:48
.= { x where x is Element of (FTSL1 n) : ex y being Element of (FTSL1 n) st
( y in U_FT (p2,i2) & x in U_FT y ) } ;
then consider x being Element of (FTSL1 n) such that
A64: x = j3 and
A65: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,i2) & x in U_FT y ) by A63;
consider y being Element of (FTSL1 n) such that
A66: y in U_FT (p2,i2) and
A67: x in U_FT y by A65;
y in Seg n by A1;
then reconsider iy = y as Nat ;
x in U_FT (y,0) by A67, FINTOPO3:47;
then A68: |.(iy - j3).| <= 1 by A46, A64;
|.(jn3 - iy).| <= i2 + 1 by A61, A62, A66;
then A69: |.(jn3 - iy).| + |.(iy - j3).| <= (i2 + 1) + 1 by A68, XREAL_1:7;
|.((jn3 - iy) + (iy - j3)).| <= |.(jn3 - iy).| + |.(iy - j3).| by COMPLEX1:56;
hence |.(jn3 - j3).| <= (i2 + 1) + 1 by A69, XXREAL_0:2; :: thesis: verum

end;

A70: for i3 being Nat holds S₁[i3] from NAT_1:sch 2(A46, A60);
assume j in U_FT (p,k) ; :: thesis: ( j in Seg n & |.(jn - j).| <= k + 1 )
hence ( j in Seg n & |.(jn - j).| <= k + 1 ) by A2, A1, A70; :: thesis: verum

end;

hence ( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) ) by A3; :: thesis: verum