defpred S_{1}[ Nat] means ( 0 in dyadic $1 & 1 in dyadic $1 );

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by Th2, TARSKI:def 2;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A3, A1);

hence for n being Nat holds

( 0 in dyadic n & 1 in dyadic n ) ; :: thesis: verum

A1: for k being Nat st S

S

proof

A3:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: ( 0 in dyadic k & 1 in dyadic k ) ; :: thesis: S_{1}[k + 1]

dyadic k c= dyadic (k + 1) by Th5;

hence S_{1}[k + 1]
by A2; :: thesis: verum

end;assume A2: ( 0 in dyadic k & 1 in dyadic k ) ; :: thesis: S

dyadic k c= dyadic (k + 1) by Th5;

hence S

for k being Nat holds S

hence for n being Nat holds

( 0 in dyadic n & 1 in dyadic n ) ; :: thesis: verum