let R be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; 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; 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; ( ( 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 )
; (Int-mult-left R) . ((i * j),a) = (Int-mult-left R) . (i,((Int-mult-left R) . (j,a)))