let I be non empty closed_interval Subset of REAL; :: thesis: for f being HK-integrable Function of I,REAL
for r being Real st f is HK-integrable holds
( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) )
let f be HK-integrable Function of I,REAL; :: thesis: for r being Real st f is HK-integrable holds
( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) )
let r be Real; :: thesis: ( f is HK-integrable implies ( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) ) )
assume f is HK-integrable ; :: thesis: ( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) )
then consider J being Real such that
A1: for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon ;
A2: for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

proof

per cases ( r = 0 or r <> 0 ) ;

suppose A3: r = 0 ; :: thesis: for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

let epsilon be Real; :: thesis: ( epsilon > 0 implies ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon )
assume A4: epsilon > 0 ; :: thesis: ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon
set jauge = the positive-yielding Function of I,REAL;
take the positive-yielding Function of I,REAL ; :: thesis: for TD being tagged_division of I st TD is the positive-yielding Function of I,REAL -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon
for TD being tagged_division of I st TD is the positive-yielding Function of I,REAL -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

proof

let TD be tagged_division of I; :: thesis: ( TD is the positive-yielding Function of I,REAL -fine implies |.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon )
assume TD is the positive-yielding Function of I,REAL -fine ; :: thesis: |.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon
tagged_sum ((r (#) f),TD) = Sum (r * (tagged_volume (f,TD))) by Th32
.= r * (Sum (tagged_volume (f,TD))) by RVSUM_1:87
.= 0 by A3 ;
hence |.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon by A3, A4; :: thesis: verum

end;

hence for TD being tagged_division of I st TD is the positive-yielding Function of I,REAL -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon ; :: thesis: verum

end;

suppose A5: r <> 0 ; :: thesis: for epsilon being Real st epsilon > 0 holds
ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

let epsilon be Real; :: thesis: ( epsilon > 0 implies ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon )
assume A6: epsilon > 0 ; :: thesis: ex jauge being positive-yielding Function of I,REAL st
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon
set e = epsilon / |.r.|;
consider jauge being positive-yielding Function of I,REAL such that
A7: for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum (f,TD)) - J).| <= epsilon / |.r.| by A1, A5, A6;
take jauge ; :: thesis: for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon
for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon

proof

let TD be tagged_division of I; :: thesis: ( TD is jauge -fine implies |.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon )
assume A8: TD is jauge -fine ; :: thesis: |.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon
|.((r * (tagged_sum (f,TD))) - (r * J)).| = |.(r * ((tagged_sum (f,TD)) - J)).|
.= |.r.| * |.((tagged_sum (f,TD)) - J).| by COMPLEX1:65 ;
then z1: |.((r * (tagged_sum (f,TD))) - (r * J)).| <= |.r.| * (epsilon / |.r.|) by A7, A8, XREAL_1:64;
tagged_sum ((r (#) f),TD) = Sum (r * (tagged_volume (f,TD))) by Th32
.= r * (tagged_sum (f,TD)) by RVSUM_1:87 ;
hence |.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon by z1, A5, XCMPLX_1:87; :: thesis: verum

end;

hence for TD being tagged_division of I st TD is jauge -fine holds
|.((tagged_sum ((r (#) f),TD)) - (r * J)).| <= epsilon ; :: thesis: verum

end;

end;

end;

then A9: r (#) f is HK-integrable ;
then HK-integral (r (#) f) = r * J by A2, DEFCC
.= r * (HK-integral f) by A1, DEFCC ;
hence ( r (#) f is HK-integrable Function of I,REAL & HK-integral (r (#) f) = r * (HK-integral f) ) by A9; :: thesis: verum