let n be Element of NAT ; for A being non empty closed_interval Subset of REAL
for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g
let A be non empty closed_interval Subset of REAL; for f being PartFunc of REAL,(REAL n)
for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g
let f be PartFunc of REAL,(REAL n); for g being Function of A,(REAL n) st f | A = g holds
integral (f,A) = integral g
let g be Function of A,(REAL n); ( f | A = g implies integral (f,A) = integral g )
assume A1:
f | A = g
; integral (f,A) = integral g
A2:
now for k being Nat st k in dom (integral (f,A)) holds
(integral (f,A)) . k = (integral g) . klet k be
Nat;
( k in dom (integral (f,A)) implies (integral (f,A)) . k = (integral g) . k )assume A3:
k in dom (integral (f,A))
;
(integral (f,A)) . k = (integral g) . kthen reconsider i =
k as
Element of
NAT ;
dom (proj (i,n)) = REAL n
by FUNCT_2:def 1;
then
rng f c= dom (proj (i,n))
;
then A4:
dom ((proj (i,n)) * f) = dom f
by RELAT_1:27;
A =
dom g
by FUNCT_2:def 1
.=
(dom f) /\ A
by A1, RELAT_1:61
;
then
((proj (i,n)) * f) || A is
total
by A4, INTEGRA5:6, XBOOLE_1:17;
then reconsider F =
((proj (i,n)) * f) | A as
Function of
A,
REAL ;
A5:
F = (proj (i,n)) * g
by A1, Lm6;
A6:
i in Seg n
by A3, Def17;
then (integral (f,A)) . i =
integral (
((proj (i,n)) * f),
A)
by Def17
.=
integral (((proj (i,n)) * f) || A)
;
hence
(integral (f,A)) . k = (integral g) . k
by A6, A5, Def14;
verum end;
dom (integral (f,A)) =
Seg n
by Def17
.=
dom (integral g)
by Def14
;
hence
integral (f,A) = integral g
by A2, FINSEQ_1:13; verum