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

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