let n be Element of NAT ; :: thesis: for a, b, c, d, r being Real
for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))
let a, b, c, d, r be Real; :: thesis: for f being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral ((r (#) f),c,d) = r * (integral (f,c,d))
let f be PartFunc of REAL,(REAL n); :: thesis: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral ((r (#) f),c,d) = r * (integral (f,c,d)) )
assume A1: ( a <= b & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral ((r (#) f),c,d) = r * (integral (f,c,d))

A2: now :: thesis: for i being Element of NAT st i in Seg n holds
integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d))

let i be Element of NAT ; :: thesis: ( i in Seg n implies integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d)) )
set P = proj (i,n);
assume A3: i in Seg n ; :: thesis: integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d))
then A4: (proj (i,n)) * f is_integrable_on ['a,b'] by A1;
(proj (i,n)) * (f | ['a,b']) is bounded by A3, A1;
then A5: ((proj (i,n)) * f) | ['a,b'] is bounded by RELAT_1:83;
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A6: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
(proj (i,n)) * (r (#) f) = r (#) ((proj (i,n)) * f) by INTEGR15:16;
hence integral (((proj (i,n)) * (r (#) f)),c,d) = r * (integral (((proj (i,n)) * f),c,d)) by A4, A5, A6, A1, INTEGRA6:25; :: thesis: verum

end;

A7: now :: thesis: for i being Nat st i in dom (integral ((r (#) f),c,d)) holds
(integral ((r (#) f),c,d)) . i = (r * (integral (f,c,d))) . i

let i be Nat; :: thesis: ( i in dom (integral ((r (#) f),c,d)) implies (integral ((r (#) f),c,d)) . i = (r * (integral (f,c,d))) . i )
assume i in dom (integral ((r (#) f),c,d)) ; :: thesis: (integral ((r (#) f),c,d)) . i = (r * (integral (f,c,d))) . i
then A8: i in Seg n by INTEGR15:def 18;
set P = proj (i,n);
thus (integral ((r (#) f),c,d)) . i = integral (((proj (i,n)) * (r (#) f)),c,d) by A8, INTEGR15:def 18
.= r * (integral (((proj (i,n)) * f),c,d)) by A8, A2
.= r * ((integral (f,c,d)) . i) by A8, INTEGR15:def 18
.= (r * (integral (f,c,d))) . i by RVSUM_1:44 ; :: thesis: verum

end;

A9: Seg n = dom (integral ((r (#) f),c,d)) by INTEGR15:def 18;
len (r * (integral (f,c,d))) = n by CARD_1:def 7;
then Seg n = dom (r * (integral (f,c,d))) by FINSEQ_1:def 3;
hence integral ((r (#) f),c,d) = r * (integral (f,c,d)) by A9, A7, FINSEQ_1:13; :: thesis: verum