assume that
( W2 is_odd_substring_of W1, 0 & n1 <=len W1 )
and A46:
ex k1 being evenNat st ( n1 = k1 +(len W2) & ( for n being Nat st 1 <= n & n <=len W2 holds W1 .(k1 + n)= W2 . n ) & ( for l being evenNat 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 evenNat st ( n2 = k2 +(len W2) & ( for n being Nat st 1 <= n & n <=len W2 holds W1 .(k2 + n)= W2 . n ) & ( for l being evenNat 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 evenNat 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 evenNat st ( for n being Nat st 1 <= n & n <=len W2 holds W1 .(l + n)= W2 . n ) holds k1 <= l
byA46; consider k2 being evenNat 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 evenNat st ( for n being Nat st 1 <= n & n <=len W2 holds W1 .(l + n)= W2 . n ) holds k2 <= l
byA48; A55:
k1 <= k2
byA51, A53;
k2 <= k1
byA50, A54; hence
n1 = n2
byA49, A52, A55, XXREAL_0:1; :: thesis: verum