let x, y be Variable; :: thesis: ( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 )
thus (x '=' y) . 1 = (<*0*> ^ (<*x*> ^ <*y*>)) . 1 by FINSEQ_1:32
.= 0 by FINSEQ_1:41 ; :: thesis: (x 'in' y) . 1 = 1
thus (x 'in' y) . 1 = (<*1*> ^ (<*x*> ^ <*y*>)) . 1 by FINSEQ_1:32
.= 1 by FINSEQ_1:41 ; :: thesis: verum