defpred S₁[ Nat] means $1 * (0. L) = 0. L;
A1: S₁[ 0 ] by BINOM:12;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: S₁[i] ; :: thesis: S₁[i + 1]
thus (i + 1) * (0. L) = (0. L) + (i * (0. L)) by BINOM:def 3
.= 0. L by A3, RLVECT_1:def 4 ; :: thesis: verum

end;

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