let x, y be set ; :: thesis: ( <*x,y*> is constant implies x = y )
A1: rng <*x,y*> = rng (<*x*> ^ <*y*>) by FINSEQ_1:def 9
.= (rng <*x*>) \/ (rng <*y*>) by FINSEQ_1:31
.= (rng <*x*>) \/ {y} by FINSEQ_1:38
.= {x} \/ {y} by FINSEQ_1:38
.= {x,y} by ENUMSET1:1 ;
A2: y in {x,y} by TARSKI:def 2;
assume <*x,y*> is constant ; :: thesis: x = y
then reconsider s = <*x,y*> as constant Function ;
A3: x in {x,y} by TARSKI:def 2;
rng s is trivial ;
hence x = y by A1, A3, A2, ZFMISC_1:def 10; :: thesis: verum