let n be Element of NAT ; :: thesis: for f being PartFunc of REAL ,(REAL n)
for A being 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 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 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

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