let x, y, z, t be Variable; :: thesis: ( x 'in' y = z 'in' t implies ( x = z & y = t ) )
assume A1: x 'in' y = z 'in' t ; :: thesis: ( x = z & y = t )
A2: ( (<*1*> ^ <*x*>) ^ <*y*> = <*1*> ^ (<*x*> ^ <*y*>) & (<*1*> ^ <*z*>) ^ <*t*> = <*1*> ^ (<*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