let n be Element of NAT ; for a, b, c, d being Real
for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let a, b, c, d be Real; for f, g being PartFunc of REAL,(REAL n) st a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] holds
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
let f, g be PartFunc of REAL,(REAL n); ( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] implies integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d)) )
assume A1:
( a <= b & f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] & f | ['a,b'] is bounded & g | ['a,b'] is bounded & ['a,b'] c= dom f & ['a,b'] c= dom g & c in ['a,b'] & d in ['a,b'] )
; integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
A2:
now for i being Element of NAT st i in Seg n holds
integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d))let i be
Element of
NAT ;
( i in Seg n implies integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d)) )set P =
proj (
i,
n);
assume A3:
i in Seg n
;
integral (((proj (i,n)) * (f + g)),c,d) = (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),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;
A6:
(proj (i,n)) * g is_integrable_on ['a,b']
by A3, A1;
(proj (i,n)) * (g | ['a,b']) is
bounded
by A3, A1;
then A7:
((proj (i,n)) * g) | ['a,b'] is
bounded
by RELAT_1:83;
A8:
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then
rng f c= dom (proj (i,n))
;
then A9:
['a,b'] c= dom ((proj (i,n)) * f)
by A1, RELAT_1:27;
rng g c= dom (proj (i,n))
by A8;
then A10:
['a,b'] c= dom ((proj (i,n)) * g)
by A1, RELAT_1:27;
A11:
(proj (i,n)) * (f + g) = ((proj (i,n)) * f) + ((proj (i,n)) * g)
by INTEGR15:15;
thus
integral (
((proj (i,n)) * (f + g)),
c,
d)
= (integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d))
by A4, A5, A9, A6, A7, A10, A1, A11, INTEGRA6:24;
verum end;
A12:
now for i being Nat st i in dom (integral ((f + g),c,d)) holds
(integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . ilet i be
Nat;
( i in dom (integral ((f + g),c,d)) implies (integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . i )assume
i in dom (integral ((f + g),c,d))
;
(integral ((f + g),c,d)) . i = ((integral (f,c,d)) + (integral (g,c,d))) . ithen A13:
i in Seg n
by INTEGR15:def 18;
set P =
proj (
i,
n);
thus (integral ((f + g),c,d)) . i =
integral (
((proj (i,n)) * (f + g)),
c,
d)
by A13, INTEGR15:def 18
.=
(integral (((proj (i,n)) * f),c,d)) + (integral (((proj (i,n)) * g),c,d))
by A13, A2
.=
((integral (f,c,d)) . i) + (integral (((proj (i,n)) * g),c,d))
by A13, INTEGR15:def 18
.=
((integral (f,c,d)) . i) + ((integral (g,c,d)) . i)
by A13, INTEGR15:def 18
.=
((integral (f,c,d)) + (integral (g,c,d))) . i
by RVSUM_1:11
;
verum end;
A14:
Seg n = dom (integral ((f + g),c,d))
by INTEGR15:def 18;
len ((integral (f,c,d)) + (integral (g,c,d))) = n
by CARD_1:def 7;
then
Seg n = dom ((integral (f,c,d)) + (integral (g,c,d)))
by FINSEQ_1:def 3;
hence
integral ((f + g),c,d) = (integral (f,c,d)) + (integral (g,c,d))
by A14, A12, FINSEQ_1:13; verum