defpred S_{1}[ Nat] means $1 * (0. L) = 0. L;

A1: S_{1}[ 0 ]
by BINOM:12;

A2: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A1, A2);

hence n * (0. L) = 0. L ; :: thesis: verum

A1: S

A2: for i being Nat st S

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A3: S_{1}[i]
; :: thesis: S_{1}[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;assume A3: S

thus (i + 1) * (0. L) = (0. L) + (i * (0. L)) by BINOM:def 3

.= 0. L by A3, RLVECT_1:def 4 ; :: thesis: verum

hence n * (0. L) = 0. L ; :: thesis: verum