let R be comRing; :: thesis: for a, b being Element of R holds (a * b) ^2 = (a ^2) * (b ^2)
let a, b be Element of R; :: thesis: (a * b) ^2 = (a ^2) * (b ^2)
thus (a * b) ^2 = (a * b) * (a * b) by O_RING_1:def 1
.= a * (b * (a * b)) by GROUP_1:def 3
.= a * (b * (b * a)) by GROUP_1:def 12
.= a * ((b * b) * a) by GROUP_1:def 3
.= a * (a * (b * b)) by GROUP_1:def 12
.= (a * a) * (b * b) by GROUP_1:def 3
.= (a * a) * (b ^2) by O_RING_1:def 1
.= (a ^2) * (b ^2) by O_RING_1:def 1 ; :: thesis: verum