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 or 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 or 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 or 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 or j = 0 ) ; :: thesis: (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

per cases ( i = 0 or j = 0 ) by A1;

suppose A2: i = 0 ; :: thesis: (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

hence (Int-mult-left R) . ((i * j),a) = 0. R by Th152
.= (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) by A2, Th152 ;
:: thesis: verum

end;

suppose A3: j = 0 ; :: thesis: (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))

hence (Int-mult-left R) . ((i * j),a) = 0. R by Th152
.= (Int-mult-left R) . (i,(0. R)) by Th154
.= (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) by Th152, A3 ;
:: thesis: verum

end;

end;