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