defpred S₁[ set , set ] means $2 = 'not' (f /. $1);
A1: for k being Nat st k in Seg (len f) holds
ex x being Element of LTLB_WFF st S₁[k,x] ;
consider p being FinSequence of LTLB_WFF such that
A2: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(A1);

A3: now :: thesis: for i being Element of NAT st 1 <= i & i <= len f holds
p . i = 'not' (f /. i)

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f implies p . i = 'not' (f /. i) )
assume ( 1 <= i & i <= len f ) ; :: thesis: p . i = 'not' (f /. i)
then i in Seg (len f) ;
hence p . i = 'not' (f /. i) by A2; :: thesis: verum

end;

len p = len f by A2, FINSEQ_1:def 3;
hence ex b₁ being FinSequence of LTLB_WFF st
( len b₁ = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
b₁ . i = 'not' (f /. i) ) ) by A3; :: thesis: verum