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 + 1 & ( 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 + 1 & ( 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
A18: ex k1 being even Nat st
( n1 = k1 + 1 & ( 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
A20: ex k2 being even Nat st
( n2 = k2 + 1 & ( 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
A21: n1 = k1 + 1 and
A22: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k1 + n) = W2 . n and
A23: 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 A18;
consider k2 being even Nat such that
A24: n2 = k2 + 1 and
A25: for n being Nat st 1 <= n & n <= len W2 holds
W1 . (k2 + n) = W2 . n and
A26: 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 A20;
A27: k1 <= k2 by A23, A25;
k2 <= k1 by A22, A26;
hence n1 = n2 by A21, A24, A27, 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