:: deftheorem defines uniformly_bounded MESFUN10:def 1 :
for X being set
for F being Functional_Sequence of X,ExtREAL holds
( F is uniformly_bounded iff ex K being Real st
for n being Nat
for x being set st x in dom (F . 0) holds
|.((F . n) . x).| <= K );