theorem Th25: :: WALLIS01:28

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
( (@ ((@ x) |^ n)) | I is continuous & @ ((@ x) |^ n) is_integrable_on I & (@ ((@ x) |^ n)) | I is bounded )