let f1, f2 be FinSequence of LTLB_WFF ; :: thesis: ( len f1 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
f1 . i = 'not' (f /. i) ) & len f2 = len f & ( for i being Element of NAT st 1 <= i & i <= len f holds
f2 . i = 'not' (f /. i) ) implies f1 = f2 )
assume that
A4: len f1 = len f and
A5: for i being Element of NAT st 1 <= i & i <= len f holds
f1 . i = 'not' (f /. i) and
A6: len f2 = len f and
A7: for i being Element of NAT st 1 <= i & i <= len f holds
f2 . i = 'not' (f /. i) ; :: thesis: f1 = f2

A8: now :: thesis: for x being Element of NAT st x in dom f1 holds
f1 . x = f2 . x

let x be Element of NAT ; :: thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume A9: x in dom f1 ; :: thesis: f1 . x = f2 . x
x in Seg (len f1) by A9, FINSEQ_1:def 3;
then A10: ( 1 <= x & x <= len f ) by FINSEQ_1:1, A4;
hence f1 . x = 'not' (f /. x) by A5
.= f2 . x by A7, A10 ;
:: thesis: verum

end;

dom f1 = Seg (len f1) by FINSEQ_1:def 3
.= dom f2 by A4, A6, FINSEQ_1:def 3 ;
hence f1 = f2 by A8, PARTFUN1:5; :: thesis: verum