let R be comRing; :: thesis: for a being Element of R
for i being Integer holds (i '*' a) ^2 = (i ^2) '*' (a ^2)
let a be Element of R; :: thesis: for i being Integer holds (i '*' a) ^2 = (i ^2) '*' (a ^2)
let i be Integer; :: thesis: (i '*' a) ^2 = (i ^2) '*' (a ^2)
thus (i '*' a) ^2 = (i '*' a) * (i '*' a) by O_RING_1:def 1
.= i '*' (a * (i '*' a)) by REALALG2:5
.= i '*' ((i '*' a) * a) by GROUP_1:def 12
.= i '*' (i '*' (a * a)) by REALALG2:5
.= (i * i) '*' (a * a) by RING_3:65
.= (i ^2) '*' (a * a) by SQUARE_1:def 1
.= (i ^2) '*' (a ^2) by O_RING_1:def 1 ; :: thesis: verum