let L be non empty right_complementable associative Abelian add-associative right_zeroed distributive left_zeroed doubleLoopStr ; :: thesis: for n being Nat holds (0. L) * n = 0. L
let n be Nat; :: thesis: (0. L) * n = 0. L
defpred S₁[ Nat] means (0. L) * $1 = 0. L;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
(0. L) * (n + 1) = (n + 1) * (0. L) by BINOM:17
.= (n * (0. L)) + (1 * (0. L)) by BINOM:15
.= (n * (0. L)) + (0. L) by BINOM:13
.= 0. L by Th3 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A2: S₁[ 0 ] by BINOM:12;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
hence (0. L) * n = 0. L ; :: thesis: verum