let n be Nat; :: thesis: for G being addGroup holds n * (0_ G) = 0_ G
let G be addGroup; :: thesis: n * (0_ G) = 0_ G
defpred S₁[ Nat] means $1 * (0_ G) = 0_ G;

A1: 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 S₁[n] ; :: thesis: S₁[n + 1]
then (n + 1) * (0_ G) = (0_ G) + (0_ G) by Def7
.= 0_ G by Def4 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] by Def7;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence n * (0_ G) = 0_ G ; :: thesis: verum