theorem Th25: :: INT_7:25

for G being commutative Group
for a, b being Element of G
for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds
ord (a * b) = n * m