theorem LM83: :: DUALSP05:8

for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.a,b.] holds
ex x being Function of A,(BoundedFunctions A) st
for s being Real st s in [.a,b.] holds
( ( s = a implies x . s = [.a,b.] --> 0 ) & ( s <> a implies x . s = ([.a,s.] --> 1) +* (].s,b.] --> 0) ) )