:: deftheorem Def1 defines with_common_domain MARGREL1:def 1 :
for IT being FinSequence-membered set holds
( IT is with_common_domain iff for a, b being FinSequence st a in IT & b in IT holds
len a = len b );