let D be non empty set ; :: thesis: for a being FinSequence of D holds {a} is Element of relations_on D
let a be FinSequence of D; :: thesis: {a} is Element of relations_on D
A1: for a1, a2 being FinSequence of D st a1 in {a} & a2 in {a} holds
len a1 = len a2

proof

let a1, a2 be FinSequence of D; :: thesis: ( a1 in {a} & a2 in {a} implies len a1 = len a2 )
assume that
A2: a1 in {a} and
A3: a2 in {a} ; :: thesis: len a1 = len a2
a1 = a by A2, TARSKI:def 1;
hence len a1 = len a2 by A3, TARSKI:def 1; :: thesis: verum

end;

a in D * by FINSEQ_1:def 11;
then {a} c= D * by ZFMISC_1:31;
hence {a} is Element of relations_on D by A1, Def7; :: thesis: verum