let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: (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 ; :: thesis: verum