let n be Element of NAT ; :: thesis: for a, b being Real

for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))

let a, b be Real; :: thesis: for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))

let f be PartFunc of REAL,(REAL n); :: thesis: integral (f,b,a) = - (integral (f,a,b))

for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))

let a, b be Real; :: thesis: for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))

let f be PartFunc of REAL,(REAL n); :: thesis: integral (f,b,a) = - (integral (f,a,b))