let IT1, IT2 be odd Element of NAT ; :: thesis: ( ( not n is even & 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 ) & ( ( n is even or not n <= len W ) & IT1 = len W & IT2 = len W implies IT1 = IT2 ) )

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

assume ( not n is even & 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 A4: ( 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 ) ) ; :: 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 ( 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 ) ) ; :: thesis: IT1 = IT2
then ( IT1 <= IT2 & IT2 <= IT1 ) by A4;
hence IT1 = IT2 by XXREAL_0:1; :: thesis: verum

end;

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