let n be Element of NAT ; :: thesis: for A being 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 closed-interval Subset of REAL ; :: thesis: 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); :: thesis: 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); :: thesis: ( f | A = g implies integral f,A = integral g )
assume A1: f | A = g ; :: thesis: integral f,A = integral g

A2: now

let k be Nat; :: thesis: ( k in dom (integral f,A) implies (integral f,A) . k = (integral g) . k )
assume A3: k in dom (integral f,A) ; :: thesis: (integral f,A) . k = (integral g) . k
then 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:46;
A = dom g by FUNCT_2:def 1
.= (dom f) /\ A by A1, RELAT_1:90 ;
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; :: thesis: 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:17; :: thesis: verum