:: deftheorem Def3 defines inf MESFUNC8:def 3 :
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b₃ being PartFunc of X,ExtREAL holds
( b₃ = inf f iff ( dom b₃ = dom (f . 0) & ( for x being Element of X st x in dom b₃ holds
b₃ . x = inf (f # x) ) ) );