let D be non empty set ; for x, y being Element of D holds {<*x,y*>} is Element of relations_on D
let x, y be Element of D; {<*x,y*>} is Element of relations_on D
A1:
for a1, a2 being FinSequence of D st a1 in {<*x,y*>} & a2 in {<*x,y*>} holds
len a1 = len a2
<*x*> ^ <*y*> is FinSequence of D
;
then
<*x,y*> in D *
by FINSEQ_1:def 11;
then
{<*x,y*>} c= D *
by ZFMISC_1:31;
hence
{<*x,y*>} is Element of relations_on D
by A1, Def7; verum