:: deftheorem defines - MESFUN11:def 2 :
for X being non empty set
for F being Functional_Sequence of X,ExtREAL holds - F = (- 1) (#) F;