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