theorem :: INTEGRA9:24
for f, g being PartFunc of REAL,REAL
for A being non empty closed_interval Subset of REAL holds |||(f,g,A)||| = |||(g,f,A)||| ;