let x, y be set ; :: thesis: ( <*x,y*> is constant implies x = y )
assume <*x,y*> is constant ; :: thesis: x = y
then reconsider s = <*x,y*> as constant Function ;
A1: rng s is trivial ;
A2: rng <*x,y*> = rng (<*x*> ^ <*y*>) by FINSEQ_1:def 9
.= (rng <*x*>) \/ (rng <*y*>) by FINSEQ_1:44
.= (rng <*x*>) \/ {y} by FINSEQ_1:55
.= {x} \/ {y} by FINSEQ_1:55
.= {x,y} by ENUMSET1:41 ;
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence x = y by A1, A2, REALSET1:14; :: thesis: verum