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 bassume that

A1: n is odd and

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

( IT <= len W & W . IT = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT <= k ) )

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

consider IT being Nat such that

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

IT <= k ) ) from NAT_1:sch 5(A3);

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

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

IT <= k ) )

thus ( IT <= len W & W . IT = W . n ) by A4; :: thesis: for k being odd Nat st k <= len W & W . k = W . n holds

IT <= k

let k be odd Nat; :: thesis: ( k <= len W & W . k = W . n implies IT <= k )

thus ( k <= len W & W . k = W . n implies IT <= k ) by A4; :: thesis: verum

end;A1: n is odd and

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

( IT <= len W & W . IT = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

IT <= k ) )

A3: ex n being Nat st S

consider IT being Nat such that

A4: ( S

IT <= k ) ) from NAT_1:sch 5(A3);

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

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

IT <= k ) )

thus ( IT <= len W & W . IT = W . n ) by A4; :: thesis: for k being odd Nat st k <= len W & W . k = W . n holds

IT <= k

let k be odd Nat; :: thesis: ( k <= len W & W . k = W . n implies IT <= k )

thus ( k <= len W & W . k = W . n implies IT <= k ) by A4; :: thesis: verum