let f be FinSequence of LTLB_WFF ; :: thesis: for g being Function of LTLB_WFF,BOOLEAN holds
( (VAL g) . ('not' ((con (nega f)) /. (len (con (nega f))))) = 0 iff for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 0 )
let g be Function of LTLB_WFF,BOOLEAN; :: thesis: ( (VAL g) . ('not' ((con (nega f)) /. (len (con (nega f))))) = 0 iff for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 0 )
set v = VAL g;
A1: (VAL g) . H₁(f) = ((VAL g) . H₂( nega f)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= ((VAL g) . H₂( nega f)) => FALSE by LTLAXIO1:def 15 ;
A2: len f = len (nega f) by Def4;

hereby :: thesis: ( ( for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 0 ) implies (VAL g) . ('not' ((con (nega f)) /. (len (con (nega f))))) = 0 )

assume A3: (VAL g) . H₁(f) = 0 ; :: thesis: for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 0
let i be Nat; :: thesis: ( i in dom f implies (VAL g) . (f /. i) = 0 )
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
assume A4: i in dom f ; :: thesis: (VAL g) . (f /. i) = 0
then A5: ( 1 <= i & i <= len f ) by FINSEQ_3:25;
A6: i in dom (nega f) by A4, FINSEQ_3:29, A2;
then A7: (nega f) /. i = (nega f) . i1 by PARTFUN1:def 6
.= 'not' (f /. i1) by Def4, A5 ;
A8: (VAL g) . H₁(f) = ((VAL g) . H₂( nega f)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= ((VAL g) . H₂( nega f)) => FALSE by LTLAXIO1:def 15 ;
((VAL g) . (f /. i)) => FALSE = ((VAL g) . (f /. i)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= (VAL g) . ('not' (f /. i)) by LTLAXIO1:def 15
.= 1 by A8, A3, Th19, A6, A7 ;
hence (VAL g) . (f /. i) = 0 ; :: thesis: verum

end;

assume A9: for i being Nat st i in dom f holds
(VAL g) . (f /. i) = 0 ; :: thesis: (VAL g) . ('not' ((con (nega f)) /. (len (con (nega f))))) = 0
assume not (VAL g) . H₁(f) = 0 ; :: thesis: contradiction
then not (VAL g) . H₂( nega f) = 1 by A1;
then consider i being Nat such that
A10: i in dom (nega f) and
A11: not (VAL g) . ((nega f) /. i) = 1 by Th19;
A12: i <= len f by A2, A10, FINSEQ_3:25;
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
A13: 1 <= i by A10, FINSEQ_3:25;
A14: (nega f) /. i = (nega f) . i1 by A10, PARTFUN1:def 6
.= 'not' (f /. i) by Def4, A13, A12 ;
A15: ((VAL g) . (f /. i1)) => FALSE = ((VAL g) . (f /. i1)) => ((VAL g) . TFALSUM) by LTLAXIO1:def 15
.= (VAL g) . ('not' (f /. i)) by LTLAXIO1:def 15
.= 0 by A11, XBOOLEAN:def 3, A14 ;
i in dom f by A2, FINSEQ_3:29, A10;
hence contradiction by A15, A9; :: thesis: verum