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 Element of NAT st k <= len W & W . k = W . n holds
k <= IT1 ) & IT2 <= len W & W . IT2 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT2 ) 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 )

assume that
n is odd and
n <= len W ; :: thesis: ( IT1 <= len W & W . IT1 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT1 ) & IT2 <= len W & W . IT2 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT2 ) implies IT1 = IT2 )
assume that
A6: IT1 <= len W and
A7: W . IT1 = W . n and
A8: for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT1 ; :: thesis: ( IT2 <= len W & W . IT2 = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT2 ) implies IT1 = IT2 )
assume that
A9: IT2 <= len W and
A10: W . IT2 = W . n and
A11: for k being odd Element of NAT st k <= len W & W . k = W . n holds
k <= IT2 ; :: thesis: IT1 = IT2
A12: IT2 <= IT1 by A8, A9, A10;
IT1 <= IT2 by A6, A7, A11;
hence IT1 = IT2 by A12, XXREAL_0:1; :: thesis: verum

end;

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