:: deftheorem defines common_on_dom SEQFUNC:def 9 :
for D1, D2 being set
for F being Functional_Sequence of D1,D2
for X being set holds
( X common_on_dom F iff ( X <> {} & ( for n being Nat holds X c= dom (F . n) ) ) );