let r be Real; :: thesis: for j, i being Element of NAT st r <> 0 & j <= i holds
r |^ (i -' j) = (r |^ i) / (r |^ j)
let j, i be Element of NAT ; :: thesis: ( r <> 0 & j <= i implies r |^ (i -' j) = (r |^ i) / (r |^ j) )
assume that
A1: r <> 0 and
A2: j <= i ; :: thesis: r |^ (i -' j) = (r |^ i) / (r |^ j)
thus (r |^ i) / (r |^ j) = (Product (i |-> r)) / (r |^ j) by NEWTON:def 1
.= (Product (i |-> r)) / (Product (j |-> r)) by NEWTON:def 1
.= Product ((i -' j) |-> r) by A1, A2, Th14
.= r |^ (i -' j) by NEWTON:def 1 ; :: thesis: verum