let n be Nat; :: thesis: 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 )
let I be non empty closed_interval Subset of REAL; :: thesis: 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 )
let x be Function of REAL,REAL; :: thesis: ( x is continuous implies ( (@ ((@ x) |^ n)) | I is continuous & @ ((@ x) |^ n) is_integrable_on I & (@ ((@ x) |^ n)) | I is bounded ) )
assume x is continuous ; :: thesis: ( (@ ((@ x) |^ n)) | I is continuous & @ ((@ x) |^ n) is_integrable_on I & (@ ((@ x) |^ n)) | I is bounded )
then A2: (@ ((@ x) |^ n)) | REAL is continuous by Th21;
I c= REAL ;
then A4: I c= dom (@ ((@ x) |^ n)) by FUNCT_2:def 1;
(@ ((@ x) |^ n)) | I is continuous by A2;
hence ( (@ ((@ x) |^ n)) | I is continuous & @ ((@ x) |^ n) is_integrable_on I & (@ ((@ x) |^ n)) | I is bounded ) by A4, INTEGRA5:10, INTEGRA5:11; :: thesis: verum