let A be Element of LTLB_WFF ; :: thesis: nega <*A*> = <*('not' A)*>

A1: now :: thesis: for n being Element of NAT st 1 <= n & n <= len <*A*> holds
<*('not' A)*> . n = 'not' (<*A*> /. n)

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len <*A*> implies <*('not' A)*> . n = 'not' (<*A*> /. n) )
assume that
A2: 1 <= n and
A3: n <= len <*A*> ; :: thesis: <*('not' A)*> . n = 'not' (<*A*> /. n)
n <= 1 by A3, FINSEQ_1:39;
then A4: n = 1 by A2, NAT_1:25;
hence <*('not' A)*> . n = 'not' A
.= 'not' (<*A*> /. n) by FINSEQ_4:16, A4 ;
:: thesis: verum

end;

len <*('not' A)*> = 1 by FINSEQ_1:39
.= len <*A*> by FINSEQ_1:39 ;
hence nega <*A*> = <*('not' A)*> by A1, Def4; :: thesis: verum