for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n) st dom f = ['a,b'] holds
f is_integrable_on ['a,b']