let z be Element of F_Complex; :: thesis: ( z |^ 3 = z * (z ^2) & z |^ 2 = z ^2 & z |^ 2 = z * z )
thus z * (z ^2) = z * (z * z) by O_RING_1:def 1
.= z * ((z |^ 1) * z) by BINOM:8
.= z * ((z |^ 1) * (z |^ 1)) by BINOM:8
.= z * (z |^ (1 + 1)) by BINOM:10
.= (z |^ 1) * (z |^ 2) by BINOM:8
.= z |^ (2 + 1) by BINOM:10
.= z |^ 3 ; :: thesis: ( z |^ 2 = z ^2 & z |^ 2 = z * z )
z * z = (z |^ 1) * z by BINOM:8
.= (z |^ 1) * (z |^ 1) by BINOM:8
.= z |^ (1 + 1) by BINOM:10 ;
hence ( z |^ 2 = z ^2 & z |^ 2 = z * z ) by O_RING_1:def 1; :: thesis: verum