let s be natural Number ; :: thesis: ( s >= 1 implies 0 |^ s = 0 )
A0: s is Nat by TARSKI:1;
defpred S₁[ Nat] means 0 |^ $1 = 0 ;

A1: now :: thesis: for n being Nat st n >= 1 & S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( n >= 1 & S₁[n] implies S₁[n + 1] )
assume ( n >= 1 & S₁[n] ) ; :: thesis: S₁[n + 1]
0 |^ (n + 1) = (0 |^ n) * 0 by Th6
.= 0 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A2: S₁[1] ;
for n being Nat st n >= 1 holds
S₁[n] from NAT_1:sch 8(A2, A1);
hence ( s >= 1 implies 0 |^ s = 0 ) by A0; :: thesis: verum