let D be non empty set ; :: thesis: for x, y being Element of D holds {<*x,y*>} is Element of relations_on D
let x, y be Element of D; :: thesis: {<*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

proof

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

end;

<*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; :: thesis: verum