:: deftheorem defines with_the_same_dom MESFUNC8:def 1 :
for X, Y being set
for F being Functional_Sequence of X,Y holds
( F is with_the_same_dom iff rng F is with_common_domain );