take {} ; :: thesis: ( {} is FinSequence-membered & {} is with_common_domain )
thus ( ( for x being set st x in {} holds
x is FinSequence ) & ( for a, b being FinSequence st a in {} & b in {} holds
len a = len b ) ) ; :: according to FINSEQ_1:def 19,MARGREL1:def 1 :: thesis: verum