take {} ; :: thesis: {} is relation-like
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 MARGREL1:def 1 :: thesis: verum