now

let i be Nat; :: thesis: ( i in Seg 1 implies ('not' <*FALSE *>) . i = <*TRUE *> . i )
assume A1: i in Seg 1 ; :: thesis: ('not' <*FALSE *>) . i = <*TRUE *> . i
then A2: i = 1 by FINSEQ_1:4, TARSKI:def 1;
len <*FALSE *> = 1 by FINSEQ_1:def 18;
then A3: <*FALSE *> /. i = <*FALSE *> . 1 by A2, FINSEQ_4:24;
len ('not' <*FALSE *>) = 1 by FINSEQ_1:def 18;
hence ('not' <*FALSE *>) . i = ('not' <*FALSE *>) /. i by A2, FINSEQ_4:24
.= 'not' (<*FALSE *> /. i) by A1, BINARITH:def 4
.= 'not' FALSE by A3, FINSEQ_1:57
.= <*TRUE *> . i by A2, FINSEQ_1:57 ;
:: thesis: verum

end;

hence 'not' <*FALSE *> = <*TRUE *> by FINSEQ_2:139; :: thesis: verum