defpred S_{1}[ Nat] means ( $1 is odd & $1 <= len W & W . $1 = W . n );

_{1} being odd Element of NAT st b_{1} = len W )
; :: thesis: verum

hereby :: thesis: ( ( not n is odd or not n <= len W ) implies ex b_{1} being odd Element of NAT st b_{1} = len W )

thus
( ( not n is odd or not n <= len W ) implies ex bA1:
for k being Nat st S_{1}[k] holds

k <= len W ;

assume that

A2: n is odd and

A3: n <= len W ; :: thesis: ex IT being odd Element of NAT st

( IT <= len W & W . IT = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT ) )

A4: ex k being Nat st S_{1}[k]
by A2, A3;

consider IT being Nat such that

A5: ( S_{1}[IT] & ( for k being Nat st S_{1}[k] holds

k <= IT ) ) from NAT_1:sch 6(A1, A4);

reconsider IT = IT as odd Element of NAT by A5, ORDINAL1:def 12;

take IT = IT; :: thesis: ( IT <= len W & W . IT = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT ) )

thus ( IT <= len W & W . IT = W . n ) by A5; :: thesis: for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT

thus for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT by A5; :: thesis: verum

end;k <= len W ;

assume that

A2: n is odd and

A3: n <= len W ; :: thesis: ex IT being odd Element of NAT st

( IT <= len W & W . IT = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT ) )

A4: ex k being Nat st S

consider IT being Nat such that

A5: ( S

k <= IT ) ) from NAT_1:sch 6(A1, A4);

reconsider IT = IT as odd Element of NAT by A5, ORDINAL1:def 12;

take IT = IT; :: thesis: ( IT <= len W & W . IT = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT ) )

thus ( IT <= len W & W . IT = W . n ) by A5; :: thesis: for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT

thus for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= IT by A5; :: thesis: verum