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
{a} in relations_on D

proof

a in D * by FINSEQ_1:def 11;
then A1: {a} c= D * by ZFMISC_1:37;
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 ( a1 in {a} & a2 in {a} ) ; :: thesis: len a1 = len a2
then ( a1 = a & a2 = a ) by TARSKI:def 1;
hence len a1 = len a2 ; :: thesis: verum

end;

hence {a} in relations_on D by A1, Def8; :: thesis: verum

end;

hence {a} is Element of relations_on D ; :: thesis: verum