let x, y, z, t be Variable; ( 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 )
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 'in' y = z 'in' t
; ( x = z & y = t )
hence
( x = z & y = t )
by A1, A2, A4, A3, FINSEQ_1:33; verum