theorem Th26: :: WALLIS01:29

for r being Real
for n being Nat
for I being non empty closed_interval Subset of REAL
for x being Function of REAL,REAL st x is continuous holds
( (r (#) (@ ((@ x) |^ n))) | I is continuous & r (#) (@ ((@ x) |^ n)) is_integrable_on I & (r (#) (@ ((@ x) |^ n))) | I is bounded )