1 in Seg 1 by FINSEQ_1:3;
then A1: (Bin1 1) /. 1 = TRUE by BINARI_2:5;
ex d being Element of BOOLEAN st Bin1 1 = <*d*> by FINSEQ_2:97;
hence Bin1 1 = <*TRUE*> by A1, FINSEQ_4:16; :: thesis: verum