:: deftheorem Def2 defines with_the_same_dom MESFUNC8:def 2 :
for X, Y being set
for F being Functional_Sequence of X,Y holds
( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) );