defpred S₁[ FinSequence of D] means contradiction;
A1: for a, b being FinSequence of D st S₁[a] & S₁[b] holds
len a = len b ;
consider r being Element of relations_on D such that
A2: for a being FinSequence of D holds
( a in r iff S₁[a] ) from MARGREL1:sch 2(A1);
take r ; :: thesis: for a being FinSequence of D holds not a in r
thus for a being FinSequence of D holds not a in r by A2; :: thesis: verum