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 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 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: (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 or ( not i = 0 & not j = 0 ) ) ;

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

end;

suppose ( not i = 0 & not 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) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a))) by Lm19; :: thesis: verum

end;

end;