let IT1, IT2 be odd Element of NAT ; :: thesis: ( ( n is odd & n <= len W & IT1 <= len W & W . IT1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT1 <= k ) & IT2 <= len W & W . IT2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ) implies IT1 = IT2 ) & ( ( not n is odd or not n <= len W ) & IT1 = len W & IT2 = len W implies IT1 = IT2 ) )

IT1 <= k ) & IT2 <= len W & W . IT2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ) implies IT1 = IT2 ) & ( ( not n is odd or not n <= len W ) & IT1 = len W & IT2 = len W implies IT1 = IT2 ) )

hereby :: thesis: ( ( not n is odd or not n <= len W ) & IT1 = len W & IT2 = len W implies IT1 = IT2 )

thus
( ( not n is odd or not n <= len W ) & IT1 = len W & IT2 = len W implies IT1 = IT2 )
; :: thesis: verumassume that

n is odd and

n <= len W ; :: thesis: ( IT1 <= len W & W . IT1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT1 <= k ) & IT2 <= len W & W . IT2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ) implies IT1 = IT2 )

assume that

A5: IT1 <= len W and

A6: W . IT1 = W . n and

A7: for k being odd Nat st k <= len W & W . k = W . n holds

IT1 <= k ; :: thesis: ( IT2 <= len W & W . IT2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ) implies IT1 = IT2 )

assume that

A8: IT2 <= len W and

A9: W . IT2 = W . n and

A10: for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ; :: thesis: IT1 = IT2

A11: IT2 <= IT1 by A5, A6, A10;

IT1 <= IT2 by A7, A8, A9;

hence IT1 = IT2 by A11, XXREAL_0:1; :: thesis: verum

end;n is odd and

n <= len W ; :: thesis: ( IT1 <= len W & W . IT1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT1 <= k ) & IT2 <= len W & W . IT2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ) implies IT1 = IT2 )

assume that

A5: IT1 <= len W and

A6: W . IT1 = W . n and

A7: for k being odd Nat st k <= len W & W . k = W . n holds

IT1 <= k ; :: thesis: ( IT2 <= len W & W . IT2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ) implies IT1 = IT2 )

assume that

A8: IT2 <= len W and

A9: W . IT2 = W . n and

A10: for k being odd Nat st k <= len W & W . k = W . n holds

IT2 <= k ; :: thesis: IT1 = IT2

A11: IT2 <= IT1 by A5, A6, A10;

IT1 <= IT2 by A7, A8, A9;

hence IT1 = IT2 by A11, XXREAL_0:1; :: thesis: verum