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