let i be Nat; :: thesis: for r being Real st r <> 0 holds
(1 / r) * (r |^ (i + 1)) = r |^ i
let r be Real; :: thesis: ( r <> 0 implies (1 / r) * (r |^ (i + 1)) = r |^ i )
assume A1: r <> 0 ; :: thesis: (1 / r) * (r |^ (i + 1)) = r |^ i
thus (1 / r) * (r |^ (i + 1)) = (1 / r) * ((r |^ i) * r) by NEWTON:6
.= ((1 / r) * r) * (r |^ i)
.= 1 * (r |^ i) by A1, XCMPLX_1:106
.= r |^ i ; :: thesis: verum