A61: 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 that
A62: ( 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 ) ) ) and
A63: ( k1 = 0 implies not g is_substring_of f,n ) and
A64: ( 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 ) ) ) and
A65: ( 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 A66: 0 + 1 <= len g by NAT_1:13;
then A67: (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 A68: ( k1 <> 0 & k2 <> 0 ) ; :: thesis: k1 = k2
then A69: k2 >= k1 by A62, A64;
k1 >= k2 by A62, A64, A68;
hence k1 = k2 by A69, XXREAL_0:1; :: thesis: verum
end;
case A70: ( k1 <> 0 & k2 = 0 ) ; :: thesis: contradiction
then A71: len g > 0 by A65, 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 that
A72: n <= i and
A73: 0 < i ; :: thesis: not f /^ (i -' 1) is_preposition_of
0 + 1 <= i by A73, NAT_1:13;
then i - 1 >= 0 by XREAL_1:50;
then A74: i -' 1 = i - 1 by XREAL_0:def 2;
(((- 1) + (len g)) + i) - i >= 0 by A67;
then A75: (((i -' 1) + (len g)) -' i) + 1 = ((len g) - 1) + 1 by A74, XREAL_0:def 2
.= ((len g) -' 1) + 1 by A67, XREAL_0:def 2 ;
A76: (i -' 1) + 1 <= (i -' 1) + (len g) by A66, XREAL_1:9;
mid (f /^ (i -' 1)),1,(len g) = ((f /^ (i -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A66, FINSEQ_6:def 3
.= (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by A61, A75, FINSEQ_5:31
.= mid f,i,((i -' 1) + (len g)) by A74, A76, FINSEQ_6:def 3 ;
then ( not 1 <= len (f /^ (i -' 1)) or not mid (f /^ (i -' 1)),1,(len g) = g ) by A65, A70, A72, A73, Th27;
hence not f /^ (i -' 1) is_preposition_of by A71, Def8; :: thesis: verum
end;
hence contradiction by A62, A70; :: thesis: verum
end;
case A77: ( k1 = 0 & k2 <> 0 ) ; :: thesis: contradiction
then A78: len g > 0 by A63, 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 that
A79: n <= i and
A80: 0 < i ; :: thesis: not f /^ (i -' 1) is_preposition_of
0 + 1 <= i by A80, NAT_1:13;
then i - 1 >= 0 by XREAL_1:50;
then A81: i -' 1 = i - 1 by XREAL_0:def 2;
(((- 1) + (len g)) + i) - i >= 0 by A67;
then A82: (((i -' 1) + (len g)) -' i) + 1 = ((len g) - 1) + 1 by A81, XREAL_0:def 2
.= ((len g) -' 1) + 1 by A67, XREAL_0:def 2 ;
A83: (i -' 1) + 1 <= (i -' 1) + (len g) by A66, XREAL_1:9;
mid (f /^ (i -' 1)),1,(len g) = ((f /^ (i -' 1)) /^ (1 -' 1)) | (((len g) -' 1) + 1) by A66, FINSEQ_6:def 3
.= (f /^ (i -' 1)) | ((((i -' 1) + (len g)) -' i) + 1) by A61, A82, FINSEQ_5:31
.= mid f,i,((i -' 1) + (len g)) by A81, A83, FINSEQ_6:def 3 ;
then ( not 1 <= len (f /^ (i -' 1)) or not mid (f /^ (i -' 1)),1,(len g) = g ) by A63, A77, A79, A80, Th27;
hence not f /^ (i -' 1) is_preposition_of by A78, Def8; :: thesis: verum
end;
hence contradiction by A64, A77; :: 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 A84: 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 A85: ( k1 <> 0 & k2 <> 0 ) ; :: thesis: k1 = k2
then A86: k2 >= k1 by A62, A64;
k1 >= k2 by A62, A64, A85;
hence k1 = k2 by A86, XXREAL_0:1; :: thesis: verum
end;
case ( k1 <> 0 & k2 = 0 ) ; :: thesis: contradiction
hence contradiction by A65, A84, Def7; :: thesis: verum
end;
case ( k1 = 0 & k2 <> 0 ) ; :: thesis: contradiction
hence contradiction by A63, A84, Def7; :: thesis: verum
end;
case ( k1 = 0 & k2 = 0 ) ; :: thesis: contradiction
hence contradiction by A63, A84, Def7; :: thesis: verum
end;
end;
end;
hence k1 = k2 ; :: thesis: verum
end;
end;
end;
hence k1 = k2 ; :: thesis: verum
end;