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 & abs (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 & abs (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 & abs (jn - j) <= k + 1 ) ) )
assume A1: p = jn ; :: thesis: ( j in U_FT p,k iff ( j in Seg n & abs (jn - j) <= k + 1 ) )
A2: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;

A3: now

assume A4: j in U_FT p,k ; :: thesis: ( j in Seg n & abs (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
abs (jn2 - j2) <= $1 + 1;
A5: 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
abs (jn2 - j2) <= 0 + 1
let p2 be Element of (FTSL1 n); :: thesis: ( jn2 = p2 & j2 in U_FT p2,0 implies abs (jn2 - j2) <= 0 + 1 )
assume A6: ( jn2 = p2 & j2 in U_FT p2,0 ) ; :: thesis: abs (jn2 - j2) <= 0 + 1
then A7: ( 1 <= jn2 & jn2 <= n ) by A2, FINSEQ_1:3;
A8: j2 in U_FT p2 by A6, FINTOPO3:47;
jn2 in NAT by ORDINAL1:def 13;
then A9: Im (Nbdl1 n),jn2 = {jn2,(max (jn2 -' 1),1),(min (jn2 + 1),n)} by A2, A6, FINTOPO4:def 3;

per cases ( j2 = jn2 or j2 = max (jn2 -' 1),1 or j2 = min (jn2 + 1),n ) by A2, A6, A8, A9, ENUMSET1:def 1;

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

hence abs (jn2 - j2) <= 0 + 1 by ABSVALUE:7; :: thesis: verum

end;

suppose A10: j2 = max (jn2 -' 1),1 ; :: thesis: abs (jn2 - j2) <= 0 + 1

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

suppose A11: jn2 -' 1 >= 1 ; :: thesis: abs (jn2 - j2) <= 0 + 1

then j2 = jn2 -' 1 by A10, XXREAL_0:def 10;
then j2 = jn2 - 1 by A11, NAT_D:39;
hence abs (jn2 - j2) <= 0 + 1 by ABSVALUE:def 1; :: thesis: verum

end;

suppose A12: jn2 -' 1 < 1 ; :: thesis: abs (jn2 - j2) <= 0 + 1

then A13: j2 = 1 by A10, XXREAL_0:def 10;
jn2 -' 1 < 0 + 1 by A12;
then jn2 -' 1 <= 0 by NAT_1:13;
then jn2 -' 1 = 0 ;
then 1 - jn2 >= 0 by NAT_D:36, XREAL_1:50;
then A14: abs (j2 - jn2) = 1 - jn2 by A13, ABSVALUE:def 1;
1 <= 1 + jn2 by NAT_1:12;
then 1 - jn2 <= (1 + jn2) - jn2 by XREAL_1:11;
hence abs (jn2 - j2) <= 0 + 1 by A14, UNIFORM1:13; :: thesis: verum

end;

end;

end;

suppose A15: j2 = min (jn2 + 1),n ; :: thesis: abs (jn2 - j2) <= 0 + 1

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

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

then j2 = jn2 + 1 by A15, XXREAL_0:def 9;
then abs (j2 - jn2) = 1 by ABSVALUE:def 1;
hence abs (jn2 - j2) <= 0 + 1 by UNIFORM1:13; :: thesis: verum

end;

suppose A16: jn2 + 1 > n ; :: thesis: abs (jn2 - j2) <= 0 + 1

then A17: j2 = n by A15, XXREAL_0:def 9;
jn2 >= n by A16, NAT_1:13;
then jn2 = n by A7, XXREAL_0:1;
hence abs (jn2 - j2) <= 0 + 1 by A17, ABSVALUE:7; :: thesis: verum

end;

end;

end;

end;

end;

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

proof

let i2 be Nat; :: thesis: ( S₁[i2] implies S₁[i2 + 1] )
assume A19: 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
abs (jn3 - j3) <= (i2 + 1) + 1
let p2 be Element of (FTSL1 n); :: thesis: ( jn3 = p2 & j3 in U_FT p2,(i2 + 1) implies abs (jn3 - j3) <= (i2 + 1) + 1 )
assume A20: ( jn3 = p2 & j3 in U_FT p2,(i2 + 1) ) ; :: thesis: abs (jn3 - j3) <= (i2 + 1) + 1
i2 in NAT by ORDINAL1:def 13;
then 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
A21: ( x = j3 & ex y being Element of (FTSL1 n) st
( y in U_FT p2,i2 & x in U_FT y ) ) by A20;
consider y being Element of (FTSL1 n) such that
A22: ( y in U_FT p2,i2 & x in U_FT y ) by A21;
y in Seg n by A2;
then reconsider iy = y as Element of NAT ;
A23: abs (jn3 - iy) <= i2 + 1 by A19, A20, A22;
x in U_FT y,0 by A22, FINTOPO3:47;
then abs (iy - j3) <= 1 by A5, A21;
then A24: (abs (jn3 - iy)) + (abs (iy - j3)) <= (i2 + 1) + 1 by A23, XREAL_1:9;
abs ((jn3 - iy) + (iy - j3)) <= (abs (jn3 - iy)) + (abs (iy - j3)) by COMPLEX1:142;
hence abs (jn3 - j3) <= (i2 + 1) + 1 by A24, XXREAL_0:2; :: thesis: verum

end;

for i3 being Nat holds S₁[i3] from NAT_1:sch 2(A5, A18);
hence ( j in Seg n & abs (jn - j) <= k + 1 ) by A1, A2, A4; :: thesis: verum

end;

now

assume A25: ( j in Seg n & abs (jn - j) <= k + 1 ) ; :: thesis: 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 & abs (jn2 - j2) <= $1 + 1 holds
j2 in U_FT p2,$1;
A26: S₁[ 0 ]

proof

let j2, jn2 be Nat; :: thesis: for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in Seg n & abs (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 & abs (jn2 - j2) <= 0 + 1 implies j2 in U_FT p2,0 )
A27: ( j2 in NAT & jn2 in NAT ) by ORDINAL1:def 13;
assume A28: ( jn2 = p2 & j2 in Seg n & abs (jn2 - j2) <= 0 + 1 ) ; :: thesis: j2 in U_FT p2,0
then A29: ( 1 <= j2 & j2 <= n ) by FINSEQ_1:3;

now

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

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

A31: jn2 - j2 <= 1 by A28, ABSVALUE:def 1;
A32: jn2 - j2 = jn2 -' j2 by A30, XREAL_0:def 2;
( jn2 -' j2 >= 0 + 1 or jn2 -' j2 = 0 ) by NAT_1:13;
then A33: ( jn2 - j2 = 1 or jn2 -' j2 = 0 ) by A31, A32, XXREAL_0:1;

per cases ( jn2 - 1 = j2 or jn2 = j2 ) by A32, A33;

suppose A34: 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 A29, A34, 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 A35: jn2 - j2 < 0 ; :: thesis: ( j2 = jn2 or j2 = max (jn2 -' 1),1 or j2 = min (jn2 + 1),n )

then - (jn2 - j2) <= 1 by A28, ABSVALUE:def 1;
then A36: (j2 - jn2) + jn2 <= 1 + jn2 by XREAL_1:9;
(jn2 - j2) + j2 < 0 + j2 by A35, XREAL_1:10;
then jn2 + 1 <= j2 by NAT_1:13;
then jn2 + 1 = j2 by A36, XXREAL_0:1;
hence ( j2 = jn2 or j2 = max (jn2 -' 1),1 or j2 = min (jn2 + 1),n ) by A29, XXREAL_0:def 9; :: thesis: verum

end;

end;

end;

then j2 in {jn2,(max (jn2 -' 1),1),(min (jn2 + 1),n)} by ENUMSET1:def 1;
then j2 in U_FT p2 by A2, A27, A28, FINTOPO4:def 3;
hence j2 in U_FT p2,0 by FINTOPO3:47; :: thesis: verum

end;

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

proof

let jj be Nat; :: thesis: ( S₁[jj] implies S₁[jj + 1] )
assume A38: 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 & abs (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 & abs (jn2 - j2) <= (jj + 1) + 1 implies j2 in U_FT p2,(jj + 1) )
assume A39: ( jn2 = p2 & j2 in Seg n & abs (jn2 - j2) <= (jj + 1) + 1 ) ; :: thesis: j2 in U_FT p2,(jj + 1)
then reconsider x0 = j2 as Element of (FTSL1 n) by A2;
A40: ( 1 <= j2 & j2 <= n ) by A39, FINSEQ_1:3;
A41: ( 1 <= jn2 & jn2 <= n ) by A2, A39, FINSEQ_1:3;

A42: now

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

suppose A43: 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 A43;

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

then A45: abs (jn2 - j2) <= jj + 1 by ABSVALUE:def 1;
FTSL1 n is filled by FINTOPO4:18;
then ( p2 in U_FT p2,jj & x0 in U_FT p2 ) by A38, A39, A44, A45, FIN_TOPO:def 4;
hence ex y being Element of (FTSL1 n) st
( y in U_FT p2,jj & x0 in U_FT y ) ; :: thesis: verum

end;

suppose A46: 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 A47: jn2 - j2 >= 0 + 1 by A46, NAT_1:13;
then A48: (jn2 - j2) + j2 >= 1 + j2 by XREAL_1:9;
j2 < j2 + 1 by NAT_1:13;
then A49: jn2 - (j2 + 1) < jn2 - j2 by XREAL_1:17;
abs (jn2 - j2) = jn2 - j2 by A46, ABSVALUE:def 1;
then A50: jn2 - (j2 + 1) < (jj + 1) + 1 by A39, A49, XXREAL_0:2;
A51: (jn2 - j2) - 1 >= 1 - 1 by A47, XREAL_1:11;
then jn2 -' (j2 + 1) = jn2 - (j2 + 1) by XREAL_0:def 2;
then A52: jn2 - (j2 + 1) <= jj + 1 by A50, NAT_1:13;
A53: n >= j2 + 1 by A41, A48, XXREAL_0:2;
1 <= j2 + 1 by A40, NAT_1:13;
then A54: j2 + 1 in Seg n by A53;
then reconsider yj2 = j2 + 1 as Element of (FTSL1 n) by A2;
A55: abs (jn2 - (j2 + 1)) <= jj + 1 by A51, A52, ABSVALUE:def 1;
abs ((j2 + 1) - j2) = 1 by ABSVALUE:def 1;
then x0 in U_FT yj2,0 by A26, A39;
then ( yj2 in U_FT p2,jj & x0 in U_FT yj2 ) by A38, A39, A54, A55, FINTOPO3:47;
hence ex y being Element of (FTSL1 n) st
( y in U_FT p2,jj & x0 in U_FT y ) ; :: 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 A56: (jn2 - j2) + j2 < 0 + j2 by XREAL_1:8;
then jn2 + 1 <= j2 by NAT_1:13;
then A57: (jn2 + 1) - 1 <= j2 - 1 by XREAL_1:11;
then A58: (j2 - 1) - jn2 >= 0 by XREAL_1:50;
j2 - 1 >= 0 by A40, XREAL_1:50;
then A59: j2 - 1 = j2 -' 1 by XREAL_0:def 2;
then A60: j2 -' 1 >= 1 by A41, A57, XXREAL_0:2;
j2 < j2 + 1 by NAT_1:13;
then j2 - 1 < (j2 + 1) - 1 by XREAL_1:11;
then j2 -' 1 < n by A40, A59, XXREAL_0:2;
then A61: j2 -' 1 in Seg n by A60;
then reconsider pj21 = j2 -' 1 as Element of (FTSL1 n) by A2;
A62: abs ((j2 -' 1) - jn2) = (j2 -' 1) - jn2 by A58, A59, ABSVALUE:def 1;
A63: j2 - jn2 > 0 by A56, XREAL_1:52;
abs (jn2 - j2) = abs (j2 - jn2) by UNIFORM1:13
.= 1 + ((j2 -' 1) - jn2) by A59, A63, ABSVALUE:def 1
.= 1 + (abs (jn2 - (j2 -' 1))) by A62, UNIFORM1:13 ;
then A64: abs (jn2 - (j2 -' 1)) <= jj + 1 by A39, XREAL_1:8;
abs ((j2 -' 1) - j2) = abs (j2 - (j2 -' 1)) by UNIFORM1:13
.= 1 by A59, ABSVALUE:def 1 ;
then x0 in U_FT pj21,0 by A26, A39;
then ( pj21 in U_FT p2,jj & x0 in U_FT pj21 ) by A38, A39, A61, A64, FINTOPO3:47;
hence ex y being Element of (FTSL1 n) st
( y in U_FT p2,jj & x0 in U_FT y ) ; :: thesis: verum

end;

end;

end;

jj in NAT by ORDINAL1:def 13;
then 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 A42; :: thesis: verum

end;

for ii being Nat holds S₁[ii] from NAT_1:sch 2(A26, A37);
hence j in U_FT p,k by A1, A25; :: thesis: verum

end;

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