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 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 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: (Int-mult-left R) . ((i + j),a) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a))

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;
A2: i + j is Element of INT by INT_1:def 2;
thus (Int-mult-left R) . ((i + j),a) = (i1 + j1) * a by A2, Def23
.= (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 = - i as Element of NAT by INT_1:3;
reconsider j1 = - j as Element of NAT by A3, INT_1:3;
A4: - (i + j) = i1 + j1 ;
A5: i + j is Element of INT by INT_1:def 2;
thus (Int-mult-left R) . ((i + j),a) = (i1 + j1) * (- a) by A3, A4, A5, Def23
.= (i1 * (- a)) + (j1 * (- a)) by BINOM:15
.= ((Int-mult-left R) . (i,a)) + ((Nat-mult-left R) . (j1,(- a))) by A3, Def23
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (j,a)) by A3, Def23 ; :: thesis: verum

end;

end;