let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; 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; 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 ; (Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))
defpred S1[ Nat] means (Nat-mult-left R) . (($1 * j),a) = (Nat-mult-left R) . ($1,((Nat-mult-left R) . (j,a)));
A1:
S1[ 0 ]
A2:
for n being Nat st S1[n] holds
S1[n + 1]
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
hence
(Nat-mult-left R) . ((i * j),a) = (Nat-mult-left R) . (i,((Nat-mult-left R) . (j,a)))
; verum