let w, x, y, z be object ; :: thesis: ( <*w,x,y,z*> is constant implies ( w = x & x = y & y = z ) )
assume A1: <*w,x,y,z*> is constant ; :: thesis: ( w = x & x = y & y = z )
then A2: <*w,x,y*> is constant by SPRECT_1:1;
<*w,x,y,z*> = <*w,x*> ^ <*y,z*> by FINSEQ_4:74;
then <*y,z*> is constant by A1, SPRECT_1:1;
hence ( w = x & x = y & y = z ) by A2, SPRECT_1:2, SPRECT_1:3; :: thesis: verum