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.Ring 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.Ring 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.Ring; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))
reconsider ii = i, jj = j as Element of INT ;

per cases ( ( i in NAT & j in NAT ) or ( i in NAT & not j in NAT ) or ( not i in NAT & j in NAT ) or ( not i in NAT & not j in NAT ) ) ;

suppose A1: ( i in NAT & 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 ;
reconsider j1 = j as Element of NAT by A1;
thus (Int-mult-left R) . ((i + j),a) = (Nat-mult-left R) . ((i1 + j1),a) by Def23
.= (i1 + j1) * a
.= (i1 * a) + (j1 * a) by BINOM:15
.= ((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 Def23 ; :: thesis: verum

end;

suppose ( 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))

hence (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) by Th158; :: thesis: verum

end;

suppose ( not i in NAT & j in NAT ) ; :: thesis: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

hence (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) by Th158; :: thesis: verum

end;

suppose ( not 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 A3: ( i < 0 & j < 0 ) by INT_1:3;
then reconsider i1 = - ii as Element of NAT by INT_1:3;
reconsider j1 = - jj as Element of NAT by A3, INT_1:3;
S1: (Int-mult-left R) . (i,a) = (Nat-mult-left R) . ((- i),(- a)) by A3, Def23
.= i1 * (- a) ;
S2: (Nat-mult-left R) . ((- j),(- a)) = j1 * (- a) ;
thus (Int-mult-left R) . ((i + j),a) = (Nat-mult-left R) . ((- (i + j)),(- a)) by Def23, A3
.= (i1 + j1) * (- a)
.= (i1 * (- a)) + (j1 * (- a)) by BINOM:15
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) by A3, Def23, S1, S2 ; :: thesis: verum

end;

end;