A50: 1 -' 1 = 1 - 1 by XREAL_0:def 2;
thus for k1, k2 being Element of NAT st ( k1 <> 0 implies ( n <= k1 & f /^ (k1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= k1 ) ) ) & ( k1 = 0 implies not g is_substring_of f,n ) & ( k2 <> 0 implies ( n <= k2 & f /^ (k2 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= k2 ) ) ) & ( k2 = 0 implies not g is_substring_of f,n ) holds
k1 = k2 :: thesis: verum

proof

let k1, k2 be Element of NAT ; :: thesis: ( ( k1 <> 0 implies ( n <= k1 & f /^ (k1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= k1 ) ) ) & ( k1 = 0 implies not g is_substring_of f,n ) & ( k2 <> 0 implies ( n <= k2 & f /^ (k2 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= k2 ) ) ) & ( k2 = 0 implies not g is_substring_of f,n ) implies k1 = k2 )
assume A51: ( ( k1 <> 0 implies ( n <= k1 & f /^ (k1 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= k1 ) ) ) & ( k1 = 0 implies not g is_substring_of f,n ) & ( k2 <> 0 implies ( n <= k2 & f /^ (k2 -' 1) is_preposition_of & ( for j being Element of NAT st j >= n & j > 0 & f /^ (j -' 1) is_preposition_of holds
j >= k2 ) ) ) & ( k2 = 0 implies not g is_substring_of f,n ) ) ; :: thesis: k1 = k2

now

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

case len g > 0 ; :: thesis: k1 = k2

then A52: 0 + 1 <= len g by NAT_1:13;
then A53: (len g) - 1 >= 0 by XREAL_1:50;

now

per cases ( ( k1 <> 0 & k2 <> 0 ) or ( k1 <> 0 & k2 = 0 ) or ( k1 = 0 & k2 <> 0 ) or ( k1 = 0 & k2 = 0 ) ) ;

case A54: ( k1 <> 0 & k2 <> 0 ) ; :: thesis: k1 = k2

then A55: k2 >= k1 by A51;
k1 >= k2 by A51, A54;
hence k1 = k2 by A55, XXREAL_0:1; :: thesis: verum

end;

case A56: ( k1 <> 0 & k2 = 0 ) ; :: thesis: contradiction

then A57: len g > 0 by A51, Def7;
for i being Element of NAT st n <= i & 0 < i holds
not f /^ (i -' 1) is_preposition_of

proof

let i be Element of NAT ; :: thesis: ( n <= i & 0 < i implies not f /^ (i -' 1) is_preposition_of )
assume A58: ( n <= i & 0 < i ) ; :: thesis: not f /^ (i -' 1) is_preposition_of
then 0 + 1 <= i by NAT_1:13;
then i - 1 >= 0 by XREAL_1:50;
then A59: i -' 1 = i - 1 by XREAL_0:def 2;
(((- 1) + (len g)) + i) - i >= 0 by A53;
then A60: (((i -' 1) + (len g)) -' i) + 1 = ((len g) - 1) + 1 by A59, XREAL_0:def 2
.= ((len g) -' 1) + 1 by A53, XREAL_0:def 2 ;
A61: (i -' 1) + 1 <= (i -' 1) + (len g) by A52, XREAL_1:9;
mid (f /^ (i -' 1)),1,(len g) = ((f /^ (i -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A52, JORDAN3:def 1
.= (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by A50, A60, FINSEQ_5:31
.= mid f,i,((i -' 1) + (len g)) by A59, A61, JORDAN3:def 1 ;
then ( not 1 <= len (f /^ (i -' 1)) or not mid (f /^ (i -' 1)),1,(len g) = g ) by A51, A56, A58, Th27;
hence not f /^ (i -' 1) is_preposition_of by A57, Def8; :: thesis: verum

end;

hence contradiction by A51, A56; :: thesis: verum

end;

case A62: ( k1 = 0 & k2 <> 0 ) ; :: thesis: contradiction

then A63: len g > 0 by A51, Def7;
for i being Element of NAT st n <= i & 0 < i holds
not f /^ (i -' 1) is_preposition_of

proof

let i be Element of NAT ; :: thesis: ( n <= i & 0 < i implies not f /^ (i -' 1) is_preposition_of )
assume A64: ( n <= i & 0 < i ) ; :: thesis: not f /^ (i -' 1) is_preposition_of
then 0 + 1 <= i by NAT_1:13;
then i - 1 >= 0 by XREAL_1:50;
then A65: i -' 1 = i - 1 by XREAL_0:def 2;
(((- 1) + (len g)) + i) - i >= 0 by A53;
then A66: (((i -' 1) + (len g)) -' i) + 1 = ((len g) - 1) + 1 by A65, XREAL_0:def 2
.= ((len g) -' 1) + 1 by A53, XREAL_0:def 2 ;
A67: (i -' 1) + 1 <= (i -' 1) + (len g) by A52, XREAL_1:9;
mid (f /^ (i -' 1)),1,(len g) = ((f /^ (i -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A52, JORDAN3:def 1
.= (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by A50, A66, FINSEQ_5:31
.= mid f,i,((i -' 1) + (len g)) by A65, A67, JORDAN3:def 1 ;
then ( not 1 <= len (f /^ (i -' 1)) or not mid (f /^ (i -' 1)),1,(len g) = g ) by A51, A62, A64, Th27;
hence not f /^ (i -' 1) is_preposition_of by A63, Def8; :: thesis: verum

end;

hence contradiction by A51, A62; :: thesis: verum

end;

case ( k1 = 0 & k2 = 0 ) ; :: thesis: k1 = k2

hence k1 = k2 ; :: thesis: verum

end;

end;

end;

hence k1 = k2 ; :: thesis: verum

end;

case A68: len g <= 0 ; :: thesis: k1 = k2

now

per cases ( ( k1 <> 0 & k2 <> 0 ) or ( k1 <> 0 & k2 = 0 ) or ( k1 = 0 & k2 <> 0 ) or ( k1 = 0 & k2 = 0 ) ) ;

case A69: ( k1 <> 0 & k2 <> 0 ) ; :: thesis: k1 = k2

then A70: k2 >= k1 by A51;
k1 >= k2 by A51, A69;
hence k1 = k2 by A70, XXREAL_0:1; :: thesis: verum

end;

case ( k1 <> 0 & k2 = 0 ) ; :: thesis: contradiction

hence contradiction by A51, A68, Def7; :: thesis: verum

end;

case ( k1 = 0 & k2 <> 0 ) ; :: thesis: contradiction

hence contradiction by A51, A68, Def7; :: thesis: verum

end;

case ( k1 = 0 & k2 = 0 ) ; :: thesis: contradiction

hence contradiction by A51, A68, Def7; :: thesis: verum

end;

end;

end;

hence k1 = k2 ; :: thesis: verum

end;

end;

end;

hence k1 = k2 ; :: thesis: verum

end;