let n be Nat; :: thesis: for K being Ring st n >= 1 holds
(0. K) |^ n = 0. K
let K be Ring; :: thesis: ( n >= 1 implies (0. K) |^ n = 0. K )
set a1 = 0. K;
assume A2: n >= 1 ; :: thesis: (0. K) |^ n = 0. K
n - 1 in NAT by A2, INT_1:5;
then consider n1 being Nat such that
A3: n1 = n - 1 ;
(0. K) |^ n = (0. K) |^ (n1 + 1) by A3
.= ((0. K) |^ n1) * (0. K) by EC_PF_1:24 ;
hence (0. K) |^ n = 0. K ; :: thesis: verum