let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; for a being Element of R
for i, j, k being Element of NAT st i <= j & k = j - i holds
(Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))
let a be Element of R; for i, j, k being Element of NAT st i <= j & k = j - i holds
(Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))
let i, j, k be Element of NAT ; ( i <= j & k = j - i implies (Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a)) )
assume A1:
( i <= j & k = j - i )
; (Nat-mult-left R) . (k,a) = ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a))
A2: j * a =
(k + i) * a
by A1
.=
(k * a) + (i * a)
by BINOM:15
;
thus ((Nat-mult-left R) . (j,a)) - ((Nat-mult-left R) . (i,a)) =
(k * a) + ((i * a) - (i * a))
by A2, RLVECT_1:28
.=
(k * a) + (0. R)
by RLVECT_1:15
.=
(Nat-mult-left R) . (k,a)
by RLVECT_1:4
; verum