theorem Th47: :: NUMBER10:47

for k being Nat
for r being Real holds powersFS ((- (k + 1)),r,(2 * (k + 1))) = (<*((- k) to_power r)*> ^ (powersFS ((- k),r,(2 * k)))) ^ <*((k + 1) to_power r)*>