theorem Th42: :: ORDEQ_01:42

for n being non zero Element of NAT
for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n) st a < b & [.a,b.] = dom f & f | ].a,b.[ is constant holds
for x being Real st x in [.a,b.] holds
f . x = f . a