let n be Element of NAT ; :: thesis: 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; :: 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

.= dom (integral g) by Def14 ;

hence integral (f,A) = integral g by A2, FINSEQ_1:13; :: thesis: verum

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; :: 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 :: thesis: for k being Nat st k in dom (integral (f,A)) holds

(integral (f,A)) . k = (integral g) . k

dom (integral (f,A)) =
Seg n
by Def17
(integral (f,A)) . k = (integral g) . k

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: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; :: thesis: verum

end;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: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; :: thesis: verum

.= dom (integral g) by Def14 ;

hence integral (f,A) = integral g by A2, FINSEQ_1:13; :: thesis: verum