defpred S₁[ Nat] means ( 0 |^|^ (2 * $1) = 1 & 0 |^|^ ((2 * $1) + 1) = 0 );
A1: S₁[ 0 ] by Th0, Th3;

A2: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus S₁[n + 1] :: thesis: verum

proof

thus A4: 0 |^|^ (2 * (n + 1)) = 0 |^|^ (((2 * n) + 1) + 1)
.= 0 |^|^ (succ ((2 * n) + 1)) by NAT_1:def 2
.= exp (0,0) by A3, Th1
.= 1 by ORDINAL2:60 ; :: thesis: 0 |^|^ ((2 * (n + 1)) + 1) = 0
thus 0 |^|^ ((2 * (n + 1)) + 1) = 0 |^|^ (succ (2 * (n + 1))) by NAT_1:def 2
.= exp (0,1) by A4, Th1
.= 0 by ORDINAL2:63 ; :: thesis: verum

end;

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2); :: thesis: verum