theorem ch0: :: FIELD_9:2

for R being comRing
for a, b being Element of R holds (a * b) ^2 = (a ^2) * (b ^2)