theorem Th36: :: MESFUN18:36

for n being non zero Nat
for E being set
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st f = g & E c= dom f holds
( f is_uniformly_continuous_on E iff for e being Real st 0 < e holds
ex r being Real st
( 0 < r & ( for x1, x2 being Point of (CarProduct ((Seg n) --> RNS_Real))
for y1, y2 being Real st [x1,y1] in E & [x2,y2] in E & ||.(x2 - x1).|| < r & |.(y2 - y1).| < r holds
|.((g . [x2,y2]) - (g . [x1,y1])).| < e ) ) )