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

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

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 |^|^ (Segm (((2 * n) + 1) + 1))
.= 0 |^|^ (succ (Segm ((2 * n) + 1))) by NAT_1:38
.= exp (0,0) by A3, Th14
.= 1 by ORDINAL2:43 ; :: thesis: 0 |^|^ ((2 * (n + 1)) + 1) = 0
thus 0 |^|^ ((2 * (n + 1)) + 1) = 0 |^|^ (Segm ((2 * (n + 1)) + 1))
.= 0 |^|^ (succ (Segm (2 * (n + 1)))) by NAT_1:38
.= exp (0,1) by A4, Th14
.= 0 by ORDINAL2:46 ; :: thesis: verum

end;

end;

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