theorem ch1: :: FIELD_9:4

for R being comRing
for a being Element of R
for i being Integer holds (i '*' a) ^2 = (i ^2) '*' (a ^2)