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