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