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 INT st i in NAT & not j in NAT holds
(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
let a be Element of R; :: thesis: for i, j being Element of INT st i in NAT & not j in NAT holds
(Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
let i, j be Element of INT ; :: thesis: ( i in NAT & not j in NAT implies (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) )
assume A1: ( i in NAT & not j in NAT ) ; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
then reconsider i1 = i as Element of NAT ;
A2: j < 0 by A1, INT_1:3;
then reconsider j1 = - j as Element of NAT by INT_1:3;
A3: i + j is Element of INT by INT_1:def 2;

per cases ( j1 <= i1 or j1 > i1 ) ;

suppose A4: j1 <= i1 ; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

reconsider k1 = i1 - j1 as Element of NAT by A4, INT_1:5;
thus (Int-mult-left R) . ((i + j),a) = (Nat-mult-left R) . (k1,a) by A3, Def23
.= ((Nat-mult-left R) . (i1,a)) - ((Nat-mult-left R) . (j1,a)) by Th156, A4
.= ((Nat-mult-left R) . (i1,a)) + ((Nat-mult-left R) . (j1,(- a))) by Th157
.= ((Int-mult-left R) . (i,a)) + ((Nat-mult-left R) . (j1,(- a))) by Def23
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) by A2, Def23 ; :: thesis: verum

end;

suppose A5: j1 > i1 ; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

then reconsider k1 = j1 - i1 as Element of NAT by INT_1:5;
A6: i1 - j1 < 0 by A5, XREAL_1:49;
thus (Int-mult-left R) . ((i + j),a) = (Nat-mult-left R) . ((- (i1 - j1)),(- a)) by A3, A6, Def23
.= (Nat-mult-left R) . (k1,(- a))
.= ((Nat-mult-left R) . (j1,(- a))) - ((Nat-mult-left R) . (i1,(- a))) by Th156, A5
.= ((Nat-mult-left R) . (j1,(- a))) + ((Nat-mult-left R) . (i1,(- (- a)))) by Th157
.= ((Nat-mult-left R) . (j1,(- a))) + ((Nat-mult-left R) . (i1,a)) by RLVECT_1:17
.= ((Int-mult-left R) . (j,a)) + ((Nat-mult-left R) . (i1,a)) by A2, Def23
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) by Def23 ; :: thesis: verum

end;

end;