let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n)
for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let f be PartFunc of REAL,(REAL n); :: thesis: for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let A be non empty closed_interval Subset of REAL; :: thesis: for a, b being Real st A = [.a,b.] holds
integral (f,A) = integral (f,a,b)
let a, b be Real; :: thesis: ( A = [.a,b.] implies integral (f,A) = integral (f,a,b) )
assume A1: A = [.a,b.] ; :: thesis: integral (f,A) = integral (f,a,b)

A2: now :: thesis: for i being Nat st i in dom (integral (f,A)) holds
(integral (f,A)) . i = (integral (f,a,b)) . i

let i be Nat; :: thesis: ( i in dom (integral (f,A)) implies (integral (f,A)) . i = (integral (f,a,b)) . i )
assume A3: i in dom (integral (f,A)) ; :: thesis: (integral (f,A)) . i = (integral (f,a,b)) . i
then reconsider k = i as Element of NAT ;
dom (integral (f,A)) = Seg n by Def17;
then ( (integral (f,A)) . k = integral (((proj (k,n)) * f),A) & (integral (f,a,b)) . k = integral (((proj (k,n)) * f),a,b) ) by A3, Def17, Def18;
hence (integral (f,A)) . i = (integral (f,a,b)) . i by A1, INTEGRA5:19; :: thesis: verum

end;

dom (integral (f,A)) = Seg n by Def17
.= dom (integral (f,a,b)) by Def18 ;
hence integral (f,A) = integral (f,a,b) by A2, FINSEQ_1:13; :: thesis: verum