theorem Th19: :: INT_7:19

for p being Prime holds
( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )