:: deftheorem Def2 defines '*' RING_3:def 2 :
for R being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of R
for i being Integer
for b₄ being Element of R holds
( b₄ = i '*' a iff ex n being Nat st
( ( i = n & b₄ = n * a ) or ( i = - n & b₄ = - (n * a) ) ) );