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 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.Ring 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.Ring; :: thesis: ( i <> 0 & j <> 0 implies (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) )
reconsider ii = i, jj = j as Element of INT ;
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;
thus (Int-mult-left R) . ((i * j),a) = (Nat-mult-left R) . ((i1 * j1),a) by 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 & jj < 0 ) by A1, INT_1:3;
reconsider i1 = i as Element of NAT by A4;
reconsider j1 = - jj as Element of NAT by A5, INT_1:3;
a7: ii * jj < 0 by XREAL_1:132, A5;
thus (Int-mult-left R) . ((i * j),a) = (Nat-mult-left R) . ((- (i * j)),(- a)) by a7, Def23
.= (Nat-mult-left R) . ((i1 * j1),(- a))
.= (Nat-mult-left R) . (i1,((Nat-mult-left R) . ((- j),(- 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 = - ii as Element of NAT by INT_1:3;
reconsider j1 = j as Element of NAT by A8;
A11: ii * jj < 0 by A9, XREAL_1:132;
thus (Int-mult-left R) . ((i * j),a) = (Nat-mult-left R) . ((- (i * j)),(- a)) by A11, Def23
.= (Nat-mult-left R) . ((i1 * j1),(- a))
.= (Nat-mult-left R) . ((- i),((Nat-mult-left R) . (j1,(- a)))) by Th162
.= (Nat-mult-left R) . ((- i),(- ((Nat-mult-left R) . (j1,a)))) by Th157
.= (Nat-mult-left R) . ((- i),(- ((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 = - ii as Element of NAT by INT_1:3;
reconsider j1 = - jj as Element of NAT by A13, INT_1:3;
- ((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 Def23
.= (Nat-mult-left R) . ((- i),((Nat-mult-left R) . ((- j),a))) by Th162
.= (Nat-mult-left R) . ((- i),(- ((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;