:: deftheorem DEF5 defines # MEASUR11:def 1 :
for X being non empty set
for F being FinSequence of PFuncs (X,ExtREAL)
for x being Element of X
for b₄ being FinSequence of ExtREAL holds
( b₄ = F # x iff ( dom b₄ = dom F & ( for n being Element of NAT st n in dom b₄ holds
b₄ . n = (F . n) . x ) ) );