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 ) )

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_{1}[ 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_{1}[ 0 ]
_{1}[jj] holds

S_{1}[jj + 1]
_{1}[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;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

proof

A16:
for jj being Nat st S
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;

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;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) ) ) )end;

then
( jn2 in NAT & j2 in {jn2,(max ((jn2 -' 1),1)),(min ((jn2 + 1),n))} )
by ENUMSET1:def 1, ORDINAL1:def 12;per cases
( jn2 - j2 >= 0 or jn2 - j2 < 0 )
;

end;

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;

end;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;

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;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

then j2 in U_FT p2 by A1, A5, FINTOPO4:def 3;

hence j2 in U_FT (p2,0) by FINTOPO3:47; :: thesis: verum

S

proof

A45:
for ii being Nat holds S
let jj be Nat; :: thesis: ( S_{1}[jj] implies S_{1}[jj + 1] )

assume A17: S_{1}[jj]
; :: thesis: S_{1}[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;

.= { 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;assume A17: S

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 )end;

U_FT (p2,(jj + 1)) =
(U_FT (p2,jj)) ^f
by FINTOPO3:48
( y in U_FT (p2,jj) & x0 in U_FT y )

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

end;

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 )

end;

( y in U_FT (p2,jj) & x0 in U_FT y )

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

end;

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 )

( 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;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

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 )

( 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;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

suppose
jn2 - j2 < 0
; :: thesis: ex y being Element of (FTSL1 n) st

( y in U_FT (p2,jj) & x0 in U_FT y )

( 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;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

.= { 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

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

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

hence
( j in U_FT (p,k) iff ( j in Seg n & |.(jn - j).| <= k + 1 ) )
by A3; :: thesis: verumdefpred S_{1}[ 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_{1}[ 0 ]
_{1}[i2] holds

S_{1}[i2 + 1]
_{1}[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;for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in U_FT (p2,$1) holds

|.(jn2 - j2).| <= $1 + 1;

A46: S

proof

A60:
for i2 being Nat st S
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;

end;|.(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;

end;

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

end;

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

end;

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;then j2 = jn2 - 1 by A53, NAT_D:39;

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

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;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

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

end;

S

proof

A70:
for i3 being Nat holds S
let i2 be Nat; :: thesis: ( S_{1}[i2] implies S_{1}[i2 + 1] )

assume A61: S_{1}[i2]
; :: thesis: S_{1}[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;assume A61: S

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

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