let x, y, z, t be Variable; :: thesis: ( x '=' y = z '=' t implies ( x = z & y = t ) )
assume A1: x '=' y = z '=' t ; :: thesis: ( x = z & y = t )
A2: ( (<*0 *> ^ <*x*>) ^ <*y*> = <*0 *> ^ (<*x*> ^ <*y*>) & (<*0 *> ^ <*z*>) ^ <*t*> = <*0 *> ^ (<*z*> ^ <*t*>) ) by FINSEQ_1:45;
( <*x,y*> . 1 = x & <*x,y*> . 2 = y & <*z,t*> . 1 = z & <*z,t*> . 2 = t & <*x*> ^ <*y*> = <*x,y*> & <*z*> ^ <*t*> = <*z,t*> ) by FINSEQ_1:61, FINSEQ_1:def 9;
hence ( x = z & y = t ) by A1, A2, FINSEQ_1:46; :: thesis: verum