theorem Th48: :: NUMBER10:48

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