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 ) ) )
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 & abs (jn - j) <= k + 1 ) )

A3: now

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;
A4: 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 )
assume that
A5: jn2 = p2 and
A6: j2 in Seg n and
A7: abs (jn2 - j2) <= 0 + 1 ; :: thesis: j2 in U_FT p2,0
A8: j2 <= n by A6, FINSEQ_1:3;
A9: 1 <= j2 by A6, FINSEQ_1:3;

now

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:10;
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:9;
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 13;
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 & 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 that
A18: jn2 = p2 and
A19: j2 in Seg n and
A20: abs (jn2 - j2) <= (jj + 1) + 1 ; :: thesis: j2 in U_FT p2,(jj + 1)
A21: j2 <= n by A19, FINSEQ_1:3;
reconsider x0 = j2 as Element of (FTSL1 n) by A1, A19;
A22: 1 <= j2 by A19, FINSEQ_1:3;
A23: jn2 <= n by A1, A18, FINSEQ_1:3;
A24: 1 <= jn2 by A1, A18, FINSEQ_1:3;

A25: now

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, FIN_TOPO:def 4;
abs (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:9;
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:17;
abs (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:11;
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: abs (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;
abs ((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:8;
then A38: j2 - jn2 > 0 by XREAL_1:52;
j2 - 1 >= 0 by A22, XREAL_1:50;
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:11;
then (j2 - 1) - jn2 >= 0 by XREAL_1:50;
then A41: abs ((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:11;
then A42: j2 -' 1 < n by A21, A39, XXREAL_0:2;
abs (jn2 - j2) = abs (j2 - jn2) by UNIFORM1:13
.= 1 + ((j2 -' 1) - jn2) by A39, A38, ABSVALUE:def 1
.= 1 + (abs (jn2 - (j2 -' 1))) by A41, UNIFORM1:13 ;
then A43: abs (jn2 - (j2 -' 1)) <= jj + 1 by A20, XREAL_1:8;
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;
abs ((j2 -' 1) - j2) = abs (j2 - (j2 -' 1)) by UNIFORM1:13
.= 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;

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 A25; :: thesis: verum

end;

A45: for ii being Nat holds S₁[ii] from NAT_1:sch 2(A4, A16);
assume ( j in Seg n & abs (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

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;
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
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 that
A47: jn2 = p2 and
A48: j2 in U_FT p2,0 ; :: thesis: abs (jn2 - j2) <= 0 + 1
A49: j2 in U_FT p2 by A48, FINTOPO3:47;
jn2 in NAT by ORDINAL1:def 13;
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:3;

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: abs (jn2 - j2) <= 0 + 1

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

end;

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

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

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

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

end;

suppose A54: jn2 -' 1 < 1 ; :: thesis: abs (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:50;
1 <= 1 + jn2 by NAT_1:12;
then A56: 1 - jn2 <= (1 + jn2) - jn2 by XREAL_1:11;
j2 = 1 by A52, A54, XXREAL_0:def 10;
then abs (j2 - jn2) = 1 - jn2 by A55, ABSVALUE:def 1;
hence abs (jn2 - j2) <= 0 + 1 by A56, UNIFORM1:13; :: thesis: verum

end;

end;

end;

suppose A57: 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 A57, 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 A58: jn2 + 1 > n ; :: thesis: abs (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 abs (jn2 - j2) <= 0 + 1 by A59, ABSVALUE:7; :: 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
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 that
A62: jn3 = p2 and
A63: 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
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 Element of NAT ;
x in U_FT y,0 by A67, FINTOPO3:47;
then A68: abs (iy - j3) <= 1 by A46, A64;
abs (jn3 - iy) <= i2 + 1 by A61, A62, A66;
then A69: (abs (jn3 - iy)) + (abs (iy - j3)) <= (i2 + 1) + 1 by A68, 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 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 & abs (jn - j) <= k + 1 )
hence ( j in Seg n & abs (jn - j) <= k + 1 ) by A2, A1, A70; :: thesis: verum

end;

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