let X be RealNormSpace; :: thesis: for r being Real

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

let r be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

let f be PartFunc of REAL, the carrier of X; :: thesis: ( A c= dom f & f is_integrable_on A implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) )

assume A1: ( A c= dom f & f is_integrable_on A ) ; :: thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

A2: A c= dom (r (#) f) by A1, VFUNCT_1:def 4;

consider g being Function of A, the carrier of X such that

A3: ( g = f | A & g is integrable ) by A1;

A4: (r (#) f) | A = r (#) (f | A) by VFUNCT_1:31

.= r (#) g by A3, Th12 ;

r (#) g is total by VFUNCT_1:34;

then reconsider gg = r (#) g as Function of A, the carrier of X ;

( gg is integrable & integral gg = r * (integral g) ) by A3, Th4;

hence r (#) f is_integrable_on A by A4; :: thesis: integral ((r (#) f),A) = r * (integral (f,A))

thus integral ((r (#) f),A) = integral gg by A4, A2, Def8

.= r * (integral g) by A3, Th4

.= r * (integral (f,A)) by A3, A1, Def8 ; :: thesis: verum

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

let r be Real; :: thesis: for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL, the carrier of X st A c= dom f & f is_integrable_on A holds

( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

let f be PartFunc of REAL, the carrier of X; :: thesis: ( A c= dom f & f is_integrable_on A implies ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) ) )

assume A1: ( A c= dom f & f is_integrable_on A ) ; :: thesis: ( r (#) f is_integrable_on A & integral ((r (#) f),A) = r * (integral (f,A)) )

A2: A c= dom (r (#) f) by A1, VFUNCT_1:def 4;

consider g being Function of A, the carrier of X such that

A3: ( g = f | A & g is integrable ) by A1;

A4: (r (#) f) | A = r (#) (f | A) by VFUNCT_1:31

.= r (#) g by A3, Th12 ;

r (#) g is total by VFUNCT_1:34;

then reconsider gg = r (#) g as Function of A, the carrier of X ;

( gg is integrable & integral gg = r * (integral g) ) by A3, Th4;

hence r (#) f is_integrable_on A by A4; :: thesis: integral ((r (#) f),A) = r * (integral (f,A))

thus integral ((r (#) f),A) = integral gg by A4, A2, Def8

.= r * (integral g) by A3, Th4

.= r * (integral (f,A)) by A3, A1, Def8 ; :: thesis: verum