let X be set ; :: thesis: ( X is empty implies X is with_common_domain )
assume A1: X is empty ; :: thesis: X is with_common_domain
then for a, b being FinSequence st a in X & b in X holds
len a = len b ;
hence X is with_common_domain by Def1, A1; :: thesis: verum