let n1, n2 be odd Element of NAT ; :: thesis: ( ( W2 is_odd_substring_of W1, 0 & n1 <= len W1 & ex k being even Nat st
( n1 = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) & n2 <= len W1 & ex k being even Nat st
( n2 = k + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k <= l ) ) implies n1 = n2 ) & ( not W2 is_odd_substring_of W1, 0 & n1 = len W1 & n2 = len W1 implies n1 = n2 ) )

hereby :: thesis: ( not W2 is_odd_substring_of W1, 0 & n1 = len W1 & n2 = len W1 implies n1 = n2 )

assume that
( W2 is_odd_substring_of W1, 0 & n1 <= len W1 ) and
A46: ex k1 being even Nat st
( n1 = k1 + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k1 + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k1 <= l ) ) and
n2 <= len W1 and
A48: ex k2 being even Nat st
( n2 = k2 + (len W2) & ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k2 + n) = W2 . n ) & ( for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k2 <= l ) ) ; :: thesis: n1 = n2
consider k1 being even Nat such that
A49: n1 = k1 + (len W2) and
A50: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k1 + n) = W2 . n and
A51: for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k1 <= l by A46;
consider k2 being even Nat such that
A52: n2 = k2 + (len W2) and
A53: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k2 + n) = W2 . n and
A54: for l being even Nat st ( for n being Nat st 1 <= n & n <= len W2 holds
W1 . (l + n) = W2 . n ) holds
k2 <= l by A48;
A55: k1 <= k2 by A51, A53;
k2 <= k1 by A50, A54;
hence n1 = n2 by A49, A52, A55, XXREAL_0:1; :: thesis: verum

end;

assume ( not W2 is_odd_substring_of W1, 0 & n1 = len W1 & n2 = len W1 ) ; :: thesis: n1 = n2
hence n1 = n2 ; :: thesis: verum