theorem Th1: :: PDLAX:1

for a, b, C being Real
for u being PartFunc of REAL,REAL st a < b & ['a,b'] c= dom u & u is continuous & ( for t being Real st t in ].a,b.[ holds
u . t = C ) holds
for t being Real st t in ['a,b'] holds
u . t = C