let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for a, b being Element of R
for i being Element of INT.Ring holds (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
let a, b be Element of R; :: thesis: for i being Element of INT.Ring holds (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
let i be Element of INT.Ring; :: thesis: (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))
reconsider ii = i as Element of INT ;

per cases ( 0 <= i or 0 > i ) ;

suppose 0 <= i ; :: thesis: (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))

then reconsider i1 = i as Element of NAT by INT_1:3;
thus (Int-mult-left R) . (i,(a + b)) = (Nat-mult-left R) . (i1,(a + b)) by Def23
.= (i1 * a) + (i1 * b) by Th160
.= ((Int-mult-left R) . (i,a)) + ((Nat-mult-left R) . (i1,b)) by Def23
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b)) by Def23 ; :: thesis: verum

end;

suppose A1: 0 > i ; :: thesis: (Int-mult-left R) . (i,(a + b)) = ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b))

then reconsider i1 = - ii as Element of NAT by INT_1:3;
(a + b) + ((- a) + (- b)) = ((b + a) + (- a)) + (- b) by RLVECT_1:def 3
.= (b + (a + (- a))) + (- b) by RLVECT_1:def 3
.= (b + (0. R)) + (- b) by RLVECT_1:5
.= b + (- b) by RLVECT_1:4
.= 0. R by RLVECT_1:5 ;
then A2: - (a + b) = (- a) + (- b) by RLVECT_1:6;
S1: i1 * (- a) = (Nat-mult-left R) . ((- i),(- a))
.= (Int-mult-left R) . (i,a) by A1, Def23 ;
S2: i1 * (- b) = (Nat-mult-left R) . ((- i),(- b)) ;
thus (Int-mult-left R) . (i,(a + b)) = (Nat-mult-left R) . ((- i),(- (a + b))) by Def23, A1
.= (i1 * (- a)) + (i1 * (- b)) by A2, Th160
.= ((Int-mult-left R) . (i,a)) + ((Int-mult-left R) . (i,b)) by A1, Def23, S1, S2 ; :: thesis: verum

end;

end;