let R be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for i being Element of NAT holds (Nat-mult-left R) . (i,(0. R)) = 0. R
let i be Element of NAT ; :: thesis: (Nat-mult-left R) . (i,(0. R)) = 0. R
defpred S₁[ Nat] means (Nat-mult-left R) . ($1,(0. R)) = 0. R;
A1: S₁[ 0 ] by BINOM:def 3;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(Nat-mult-left R) . ((n + 1),(0. R)) = (0. R) + (0. R) by A3, BINOM:def 3
.= 0. R by RLVECT_1:4 ;
hence S₁[n + 1] ; :: thesis: verum

end;

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