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) = j '*' (i '*' a)
let a be Element of R; :: thesis: for i, j being Integer holds i '*' (j '*' a) = j '*' (i '*' a)
let i, j be Integer; :: thesis: i '*' (j '*' a) = j '*' (i '*' a)
thus i '*' (j '*' a) = (i * j) '*' a by Th64
.= j '*' (i '*' a) by Th64 ; :: thesis: verum