let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for a being Element of R
for i, j being Element of NAT holds (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))
let a be Element of R; :: thesis: for i, j being Element of NAT holds (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))
let i, j be Element of NAT ; :: thesis: (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))
defpred S₁[ Element of NAT ] means (Nat-mult-left R) . (($1 * j),a) = (Nat-mult-left R) . ($1,((Nat-mult-left R) . (j,a)));
A1: S₁[ 0 ]

proof

(Nat-mult-left R) . ((0 * j),a) = 0. R by BINOM:def 3
.= (Nat-mult-left R) . (0,((Nat-mult-left R) . (j,a))) by BINOM:def 3 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(Nat-mult-left R) . (((n + 1) * j),a) = (j + (n * j)) * a
.= (j * a) + ((n * j) * a) by BINOM:15
.= (Nat-mult-left R) . ((n + 1),(j * a)) by A3, BINOM:def 3 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a))) ; :: thesis: verum