let R be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of R
for i, j being Integer holds (i - j) '*' a = (i '*' a) - (j '*' a)
let a be Element of R; :: thesis: for i, j being Integer holds (i - j) '*' a = (i '*' a) - (j '*' a)
let i, j be Integer; :: thesis: (i - j) '*' a = (i '*' a) - (j '*' a)
thus (i - j) '*' a = (i '*' a) + ((0 - j) '*' a) by Th61
.= (i '*' a) - (j '*' a) by Th62 ; :: thesis: verum