now :: thesis: for i being Nat st i in Seg 1 holds
('not' <*FALSE*>) . i = <*TRUE*> . i

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:2, TARSKI:def 1;
len <*FALSE*> = 1 by CARD_1:def 7;
then A3: <*FALSE*> /. i = <*FALSE*> . 1 by A2, FINSEQ_4:15;
len ('not' <*FALSE*>) = 1 by CARD_1:def 7;
hence ('not' <*FALSE*>) . i = ('not' <*FALSE*>) /. i by A2, FINSEQ_4:15
.= 'not' (<*FALSE*> /. i) by A1, BINARITH:def 1
.= 'not' FALSE by A3
.= <*TRUE*> . i by A2 ;
:: thesis: verum

end;

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