A1:
1 -' 1 = 1 - 1
by XREAL_0:def 2;

_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )
; :: thesis: verum

now :: thesis: ( ( g is_substring_of f,n & ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) ) ) or ( not g is_substring_of f,n & ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) ) ) )end;

hence
ex b( ( b

j >= b

( ( b

j >= b

per cases
( g is_substring_of f,n or not g is_substring_of f,n )
;

end;

case A2:
g is_substring_of f,n
; :: thesis: ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )

_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )
; :: thesis: verum

end;

( ( b

j >= b

now :: thesis: ( ( len g > 0 & ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) ) ) or ( len g <= 0 & ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) ) ) )end;

hence
ex b( ( b

j >= b

( ( b

j >= b

per cases
( len g > 0 or len g <= 0 )
;

end;

case A3:
len g > 0
; :: thesis: ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )

( ( b

j >= b

A5:
0 + 1 <= len g
by A3, NAT_1:13;

_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )
; :: thesis: verum

end;now :: thesis: ( ( n > 0 & ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) ) ) or ( n = 0 & ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) ) ) )end;

hence
ex b( ( b

j >= b

( ( b

j >= b

per cases
( n > 0 or n = 0 )
;

end;

case A6:
n > 0
; :: thesis: ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )

( ( b

j >= b

defpred S_{1}[ Nat] means ( n <= $1 & $1 <= len f & mid (f,$1,(($1 -' 1) + (len g))) = g );

A7: ex i being Nat st S_{1}[i]
by A2, A3;

ex k being Nat st

( S_{1}[k] & ( for m being Nat st S_{1}[m] holds

m >= k ) ) from NAT_1:sch 5(A7);

then consider k0 being Nat such that

A8: n <= k0 and

A9: k0 <= len f and

A10: mid (f,k0,((k0 -' 1) + (len g))) = g and

A11: for m being Nat st n <= m & m <= len f & mid (f,m,((m -' 1) + (len g))) = g holds

m >= k0 ;

reconsider k0 = k0 as Element of NAT by ORDINAL1:def 12;

0 + 1 <= k0 by A6, A8, NAT_1:13;

then A12: k0 -' 1 = k0 - 1 by XREAL_0:def 2, XREAL_1:48;

k0 - 1 < (k0 + 1) - 1 by XREAL_1:9, XREAL_1:29;

then k0 -' 1 < len f by A9, A12, XXREAL_0:2;

then A13: len (f /^ (k0 -' 1)) = (len f) - (k0 -' 1) by RFINSEQ:def 1;

(len f) - k0 >= 0 by A9, XREAL_1:48;

then A14: ((len f) - k0) + 1 >= 0 + 1 by XREAL_1:7;

A15: 1 -' 1 = 1 - 1 by XREAL_0:def 2;

A16: 0 + 1 <= len g by A3, NAT_1:13;

then A17: (k0 -' 1) + 1 <= (k0 -' 1) + (len g) by XREAL_1:7;

A18: (len g) - 1 >= 0 by A16, XREAL_1:48;

then (((- 1) + (len g)) + k0) - k0 >= 0 ;

then A19: (((k0 -' 1) + (len g)) -' k0) + 1 = ((len g) - 1) + 1 by A12, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A18, XREAL_0:def 2 ;

mid ((f /^ (k0 -' 1)),1,(len g)) = ((f /^ (k0 -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (k0 -' 1)) | ((((k0 -' 1) + (len g)) -' k0) + 1) by A15, A19, FINSEQ_5:28

.= mid (f,k0,((k0 -' 1) + (len g))) by A12, A17, FINSEQ_6:def 3 ;

then A20: g is_preposition_of f /^ (k0 -' 1) by A10, A12, A13, A14;

for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= k0_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )
by A6, A8, A20; :: thesis: verum

end;A7: ex i being Nat st S

ex k being Nat st

( S

m >= k ) ) from NAT_1:sch 5(A7);

then consider k0 being Nat such that

A8: n <= k0 and

A9: k0 <= len f and

A10: mid (f,k0,((k0 -' 1) + (len g))) = g and

A11: for m being Nat st n <= m & m <= len f & mid (f,m,((m -' 1) + (len g))) = g holds

m >= k0 ;

reconsider k0 = k0 as Element of NAT by ORDINAL1:def 12;

0 + 1 <= k0 by A6, A8, NAT_1:13;

then A12: k0 -' 1 = k0 - 1 by XREAL_0:def 2, XREAL_1:48;

k0 - 1 < (k0 + 1) - 1 by XREAL_1:9, XREAL_1:29;

then k0 -' 1 < len f by A9, A12, XXREAL_0:2;

then A13: len (f /^ (k0 -' 1)) = (len f) - (k0 -' 1) by RFINSEQ:def 1;

(len f) - k0 >= 0 by A9, XREAL_1:48;

then A14: ((len f) - k0) + 1 >= 0 + 1 by XREAL_1:7;

A15: 1 -' 1 = 1 - 1 by XREAL_0:def 2;

A16: 0 + 1 <= len g by A3, NAT_1:13;

then A17: (k0 -' 1) + 1 <= (k0 -' 1) + (len g) by XREAL_1:7;

A18: (len g) - 1 >= 0 by A16, XREAL_1:48;

then (((- 1) + (len g)) + k0) - k0 >= 0 ;

then A19: (((k0 -' 1) + (len g)) -' k0) + 1 = ((len g) - 1) + 1 by A12, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A18, XREAL_0:def 2 ;

mid ((f /^ (k0 -' 1)),1,(len g)) = ((f /^ (k0 -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (k0 -' 1)) | ((((k0 -' 1) + (len g)) -' k0) + 1) by A15, A19, FINSEQ_5:28

.= mid (f,k0,((k0 -' 1) + (len g))) by A12, A17, FINSEQ_6:def 3 ;

then A20: g is_preposition_of f /^ (k0 -' 1) by A10, A12, A13, A14;

for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= k0

proof

hence
ex b
let j be Element of NAT ; :: thesis: ( j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) implies j >= k0 )

assume that

A21: j >= n and

A22: j > 0 and

A23: g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= k0

A24: mid ((f /^ (j -' 1)),1,(len g)) = g by A3, A23;

end;assume that

A21: j >= n and

A22: j > 0 and

A23: g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= k0

A24: mid ((f /^ (j -' 1)),1,(len g)) = g by A3, A23;

now :: thesis: ( ( j <= len f & j >= k0 ) or ( j > len f & j >= k0 ) )end;

hence
j >= k0
; :: thesis: verumper cases
( j <= len f or j > len f )
;

end;

case A25:
j <= len f
; :: thesis: j >= k0

0 + 1 <= j
by A22, NAT_1:13;

then A26: j -' 1 = j - 1 by XREAL_0:def 2, XREAL_1:48;

(((- 1) + (len g)) + j) - j >= 0 by A18;

then A27: (((j -' 1) + (len g)) -' j) + 1 = ((len g) - 1) + 1 by A26, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A18, XREAL_0:def 2 ;

A28: (j -' 1) + 1 <= (j -' 1) + (len g) by A16, XREAL_1:7;

mid ((f /^ (j -' 1)),1,(len g)) = ((f /^ (j -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (j -' 1)) | ((((j -' 1) + (len g)) -' j) + 1) by A15, A27, FINSEQ_5:28

.= mid (f,j,((j -' 1) + (len g))) by A26, A28, FINSEQ_6:def 3 ;

hence j >= k0 by A11, A21, A24, A25; :: thesis: verum

end;then A26: j -' 1 = j - 1 by XREAL_0:def 2, XREAL_1:48;

(((- 1) + (len g)) + j) - j >= 0 by A18;

then A27: (((j -' 1) + (len g)) -' j) + 1 = ((len g) - 1) + 1 by A26, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A18, XREAL_0:def 2 ;

A28: (j -' 1) + 1 <= (j -' 1) + (len g) by A16, XREAL_1:7;

mid ((f /^ (j -' 1)),1,(len g)) = ((f /^ (j -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (j -' 1)) | ((((j -' 1) + (len g)) -' j) + 1) by A15, A27, FINSEQ_5:28

.= mid (f,j,((j -' 1) + (len g))) by A26, A28, FINSEQ_6:def 3 ;

hence j >= k0 by A11, A21, A24, A25; :: thesis: verum

( ( b

j >= b

case A29:
n = 0
; :: thesis: ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )

( ( b

j >= b

then A30:
g is_substring_of f,1
by A2, Th20;

reconsider n2 = 1 as Element of NAT ;

defpred S_{1}[ Nat] means ( n2 <= $1 & $1 <= len f & mid (f,$1,(($1 -' 1) + (len g))) = g );

A32: ex i being Nat st S_{1}[i]
by A3, A30;

ex k being Nat st

( S_{1}[k] & ( for m being Nat st S_{1}[m] holds

m >= k ) ) from NAT_1:sch 5(A32);

then consider k0 being Nat such that

A33: n2 <= k0 and

A34: k0 <= len f and

A35: mid (f,k0,((k0 -' 1) + (len g))) = g and

A36: for m being Nat st n2 <= m & m <= len f & mid (f,m,((m -' 1) + (len g))) = g holds

m >= k0 ;

reconsider k0 = k0 as Element of NAT by ORDINAL1:def 12;

A37: k0 -' 1 = k0 - 1 by XREAL_0:def 2, A33, XREAL_1:48;

k0 - 1 < (k0 + 1) - 1 by XREAL_1:9, XREAL_1:29;

then k0 -' 1 < len f by A34, A37, XXREAL_0:2;

then A38: len (f /^ (k0 -' 1)) = (len f) - (k0 -' 1) by RFINSEQ:def 1;

(len f) - k0 >= 0 by A34, XREAL_1:48;

then A39: ((len f) - k0) + 1 >= 0 + 1 by XREAL_1:7;

A40: 0 + 1 <= len g by A3, NAT_1:13;

then A41: (k0 -' 1) + 1 <= (k0 -' 1) + (len g) by XREAL_1:7;

A42: (len g) - 1 >= 0 by A40, XREAL_1:48;

then (((- 1) + (len g)) + k0) - k0 >= 0 ;

then A43: (((k0 -' 1) + (len g)) -' k0) + 1 = ((len g) - 1) + 1 by A37, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A42, XREAL_0:def 2 ;

mid ((f /^ (k0 -' 1)),1,(len g)) = ((f /^ (k0 -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (k0 -' 1)) | ((((k0 -' 1) + (len g)) -' k0) + 1) by A1, A43, FINSEQ_5:28

.= mid (f,k0,((k0 -' 1) + (len g))) by A37, A41, FINSEQ_6:def 3 ;

then A44: g is_preposition_of f /^ (k0 -' 1) by A35, A37, A38, A39;

A45: for j being Element of NAT st j >= n2 & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= k0

j >= k0_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )
by A29, A33, A44; :: thesis: verum

end;reconsider n2 = 1 as Element of NAT ;

defpred S

A32: ex i being Nat st S

ex k being Nat st

( S

m >= k ) ) from NAT_1:sch 5(A32);

then consider k0 being Nat such that

A33: n2 <= k0 and

A34: k0 <= len f and

A35: mid (f,k0,((k0 -' 1) + (len g))) = g and

A36: for m being Nat st n2 <= m & m <= len f & mid (f,m,((m -' 1) + (len g))) = g holds

m >= k0 ;

reconsider k0 = k0 as Element of NAT by ORDINAL1:def 12;

A37: k0 -' 1 = k0 - 1 by XREAL_0:def 2, A33, XREAL_1:48;

k0 - 1 < (k0 + 1) - 1 by XREAL_1:9, XREAL_1:29;

then k0 -' 1 < len f by A34, A37, XXREAL_0:2;

then A38: len (f /^ (k0 -' 1)) = (len f) - (k0 -' 1) by RFINSEQ:def 1;

(len f) - k0 >= 0 by A34, XREAL_1:48;

then A39: ((len f) - k0) + 1 >= 0 + 1 by XREAL_1:7;

A40: 0 + 1 <= len g by A3, NAT_1:13;

then A41: (k0 -' 1) + 1 <= (k0 -' 1) + (len g) by XREAL_1:7;

A42: (len g) - 1 >= 0 by A40, XREAL_1:48;

then (((- 1) + (len g)) + k0) - k0 >= 0 ;

then A43: (((k0 -' 1) + (len g)) -' k0) + 1 = ((len g) - 1) + 1 by A37, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A42, XREAL_0:def 2 ;

mid ((f /^ (k0 -' 1)),1,(len g)) = ((f /^ (k0 -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (k0 -' 1)) | ((((k0 -' 1) + (len g)) -' k0) + 1) by A1, A43, FINSEQ_5:28

.= mid (f,k0,((k0 -' 1) + (len g))) by A37, A41, FINSEQ_6:def 3 ;

then A44: g is_preposition_of f /^ (k0 -' 1) by A35, A37, A38, A39;

A45: for j being Element of NAT st j >= n2 & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= k0

proof

for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds
let j be Element of NAT ; :: thesis: ( j >= n2 & j > 0 & g is_preposition_of f /^ (j -' 1) implies j >= k0 )

assume that

A46: j >= n2 and

j > 0 and

A47: g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= k0

A48: mid ((f /^ (j -' 1)),1,(len g)) = g by A3, A47;

end;assume that

A46: j >= n2 and

j > 0 and

A47: g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= k0

A48: mid ((f /^ (j -' 1)),1,(len g)) = g by A3, A47;

now :: thesis: ( ( j <= len f & j >= k0 ) or ( j > len f & j >= k0 ) )end;

hence
j >= k0
; :: thesis: verumper cases
( j <= len f or j > len f )
;

end;

case A49:
j <= len f
; :: thesis: j >= k0

A50:
j -' 1 = j - 1
by XREAL_0:def 2, A46, XREAL_1:48;

(((- 1) + (len g)) + j) - j >= 0 by A42;

then A51: (((j -' 1) + (len g)) -' j) + 1 = ((len g) - 1) + 1 by A50, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A42, XREAL_0:def 2 ;

A52: (j -' 1) + 1 <= (j -' 1) + (len g) by A40, XREAL_1:7;

mid ((f /^ (j -' 1)),1,(len g)) = ((f /^ (j -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (j -' 1)) | ((((j -' 1) + (len g)) -' j) + 1) by A1, A51, FINSEQ_5:28

.= mid (f,j,((j -' 1) + (len g))) by A50, A52, FINSEQ_6:def 3 ;

hence j >= k0 by A36, A46, A48, A49; :: thesis: verum

end;(((- 1) + (len g)) + j) - j >= 0 by A42;

then A51: (((j -' 1) + (len g)) -' j) + 1 = ((len g) - 1) + 1 by A50, XREAL_0:def 2

.= ((len g) -' 1) + 1 by A42, XREAL_0:def 2 ;

A52: (j -' 1) + 1 <= (j -' 1) + (len g) by A40, XREAL_1:7;

mid ((f /^ (j -' 1)),1,(len g)) = ((f /^ (j -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A5, FINSEQ_6:def 3

.= (f /^ (j -' 1)) | ((((j -' 1) + (len g)) -' j) + 1) by A1, A51, FINSEQ_5:28

.= mid (f,j,((j -' 1) + (len g))) by A50, A52, FINSEQ_6:def 3 ;

hence j >= k0 by A36, A46, A48, A49; :: thesis: verum

j >= k0

proof

hence
ex b
let j be Element of NAT ; :: thesis: ( j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) implies j >= k0 )

assume that

j >= n and

A53: j > 0 and

A54: g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= k0

j >= 0 + n2 by A53, NAT_1:13;

hence j >= k0 by A45, A54; :: thesis: verum

end;assume that

j >= n and

A53: j > 0 and

A54: g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= k0

j >= 0 + n2 by A53, NAT_1:13;

hence j >= k0 by A45, A54; :: thesis: verum

( ( b

j >= b

( ( b

j >= b

case A55:
len g <= 0
; :: thesis: ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )

( ( b

j >= b

reconsider nn = max (n,1) as Element of NAT by ORDINAL1:def 12;

A56: nn >= n by XXREAL_0:25;

A57: nn >= 0 + 1 by XXREAL_0:25;

A58: g is_preposition_of f /^ (nn -' 1) by A55;

for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= nn_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )
by A56, A57, A58; :: thesis: verum

end;A56: nn >= n by XXREAL_0:25;

A57: nn >= 0 + 1 by XXREAL_0:25;

A58: g is_preposition_of f /^ (nn -' 1) by A55;

for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= nn

proof

hence
ex b
let j be Element of NAT ; :: thesis: ( j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) implies j >= nn )

assume that

A59: j >= n and

A60: j > 0 and

g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= nn

j >= 0 + 1 by A60, NAT_1:13;

hence j >= nn by A59, XXREAL_0:28; :: thesis: verum

end;assume that

A59: j >= n and

A60: j > 0 and

g is_preposition_of f /^ (j -' 1) ; :: thesis: j >= nn

j >= 0 + 1 by A60, NAT_1:13;

hence j >= nn by A59, XXREAL_0:28; :: thesis: verum

( ( b

j >= b

( ( b

j >= b

case
not g is_substring_of f,n
; :: thesis: ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )

( ( b

j >= b

hence
ex b_{1} being Element of NAT st

( ( b_{1} <> 0 implies ( n <= b_{1} & g is_preposition_of f /^ (b_{1} -' 1) & ( for j being Element of NAT st j >= n & j > 0 & g is_preposition_of f /^ (j -' 1) holds

j >= b_{1} ) ) ) & ( b_{1} = 0 implies not g is_substring_of f,n ) )
; :: thesis: verum

end;( ( b

j >= b

( ( b

j >= b