A1: 'not' . 1 = 1 by FINSEQ_1:def 8;
'&' . 1 = 2 by FINSEQ_1:def 8;
hence ( 'not' <> '&' & 'not' <> '=' & '&' <> '=' ) by A1, FINSEQ_1:def 8; :: thesis: verum