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 <> 0 & j <> 0 holds
(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))
let a be Element of R; :: thesis: for i, j being Element of INT st i <> 0 & j <> 0 holds
(Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))
let i, j be Element of INT ; :: thesis: ( i <> 0 & j <> 0 implies (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) )
assume A1: ( i <> 0 & j <> 0 ) ; :: thesis: (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((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 A2: ( i in NAT & j in NAT ) ; :: thesis: (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

then reconsider i1 = i as Element of NAT ;
reconsider j1 = j as Element of NAT by A2;
A3: i * j is Element of INT by INT_1:def 2;
thus (Int-mult-left R) . ((i * j),a) = (Nat-mult-left R) . ((i1 * j1),a) by A3, Def23
.= (Nat-mult-left R) . (i1,((Nat-mult-left R) . (j1,a))) by Th162
.= (Nat-mult-left R) . (i1,((Int-mult-left R) . (j,a))) by Def23
.= (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) by Def23 ; :: thesis: verum

end;

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

then A5: ( 0 < i & j < 0 ) by A1, INT_1:3;
reconsider i1 = i as Element of NAT by A4;
reconsider j1 = - j as Element of NAT by A5, INT_1:3;
A6: - (i * j) = i1 * j1 ;
A7: j * i < 0 * i by A5, XREAL_1:68;
i * j is Element of INT by INT_1:def 2;
hence (Int-mult-left R) . ((i * j),a) = (Nat-mult-left R) . ((i1 * j1),(- a)) by A7, A6, Def23
.= (Nat-mult-left R) . (i1,((Nat-mult-left R) . (j1,(- a)))) by Th162
.= (Nat-mult-left R) . (i1,((Int-mult-left R) . (j,a))) by Def23, A5
.= (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) by Def23 ;
:: thesis: verum

end;

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

then A9: ( 0 < j & i < 0 ) by A1, INT_1:3;
then reconsider i1 = - i as Element of NAT by INT_1:3;
reconsider j1 = j as Element of NAT by A8;
A10: - (i * j) = i1 * j1 ;
A11: i * j < 0 * j by A9, XREAL_1:68;
A12: i * j is Element of INT by INT_1:def 2;
thus (Int-mult-left R) . ((i * j),a) = (Nat-mult-left R) . ((i1 * j1),(- a)) by A11, A10, A12, Def23
.= (Nat-mult-left R) . (i1,((Nat-mult-left R) . (j1,(- a)))) by Th162
.= (Nat-mult-left R) . (i1,(- ((Nat-mult-left R) . (j1,a)))) by Th157
.= (Nat-mult-left R) . (i1,(- ((Int-mult-left R) . (j,a)))) by Def23
.= (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) by A9, Def23 ; :: 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,((Int-mult-left R) . (j,a)))

then A13: ( 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 A13, INT_1:3;
A14: i * j is Element of INT by INT_1:def 2;
- ((Nat-mult-left R) . (j1,a)) = (Nat-mult-left R) . (j1,(- a)) by Th157;
then ((Nat-mult-left R) . (j1,(- a))) + ((Nat-mult-left R) . (j1,a)) = 0. R by RLVECT_1:def 10;
then A15: (Nat-mult-left R) . (j1,a) = - ((Nat-mult-left R) . (j1,(- a))) by RLVECT_1:def 10;
thus (Int-mult-left R) . ((i * j),a) = (Nat-mult-left R) . ((i1 * j1),a) by A14, Def23
.= (Nat-mult-left R) . (i1,((Nat-mult-left R) . (j1,a))) by Th162
.= (Nat-mult-left R) . (i1,(- ((Int-mult-left R) . (j,a)))) by A13, A15, Def23
.= (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) by A13, Def23 ; :: thesis: verum

end;

end;