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