let P be consistent complete PNPair; :: thesis: for T being pnptree of P
for f being FinSequence of LTLB_WFF st rng f = (rngr T) ^ holds
{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => ('X' ('not' ((con (nega f)) /. (len (con (nega f))))))
let T be pnptree of P; :: thesis: for f being FinSequence of LTLB_WFF st rng f = (rngr T) ^ holds
{} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => ('X' ('not' ((con (nega f)) /. (len (con (nega f))))))
let f be FinSequence of LTLB_WFF ; :: thesis: ( rng f = (rngr T) ^ implies {} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => ('X' ('not' ((con (nega f)) /. (len (con (nega f)))))) )
assume A1: rng f = (rngr T) ^ ; :: thesis: {} LTLB_WFF |- ('not' ((con (nega f)) /. (len (con (nega f))))) => ('X' ('not' ((con (nega f)) /. (len (con (nega f))))))

A2: now :: thesis: for R being Element of rng T holds {} LTLB_WFF |- (R ^) => ('X' H₁(f))

let R be Element of rng T; :: thesis: {} LTLB_WFF |- (R ^) => ('X' H₁(f))
consider Q being object such that
A3: Q in untn R by XBOOLE_0:def 1;
reconsider Q = Q as Element of untn R by A3;
consider g being FinSequence such that
A4: rng g = (comp Q) ^ and
g is one-to-one by FINSEQ_4:58;
reconsider g = g as FinSequence of LTLB_WFF by A4, FINSEQ_1:def 4;
A5: {} LTLB_WFF |- (R ^) => ('X' (Q ^)) by Th18;
reconsider Q = Q as consistent PNPair ;

now :: thesis: for j being Nat st j in dom g holds
{} LTLB_WFF |- (g /. j) => H₁(f)

let j be Nat; :: thesis: ( j in dom g implies {} LTLB_WFF |- (g /. j) => H₁(f) )
assume j in dom g ; :: thesis: {} LTLB_WFF |- (g /. j) => H₁(f)
then g /. j in (comp Q) ^ by PARTFUN2:2, A4;
then consider S being PNPair such that
A6: g /. j = S ^ and
A7: S in comp Q ;
comp Q c= rngr T by Th28;
then S ^ in (rngr T) ^ by A7;
then consider k being Element of NAT such that
A8: k in dom f and
A9: f /. k = g /. j by A6, A1, PARTFUN2:2;
(f /. k) => H₁(f) is ctaut by LTLAXIO2:29, A8;
then (f /. k) => H₁(f) in LTL_axioms by LTLAXIO1:def 17;
hence {} LTLB_WFF |- (g /. j) => H₁(f) by LTLAXIO1:42, A9; :: thesis: verum

end;

then A10: {} LTLB_WFF |- H₁(g) => H₁(f) by LTLAXIO2:57;
('X' ((Q ^) => H₁(f))) => (('X' (Q ^)) => ('X' H₁(f))) in LTL_axioms by LTLAXIO1:def 17;
then A11: {} LTLB_WFF |- ('X' ((Q ^) => H₁(f))) => (('X' (Q ^)) => ('X' H₁(f))) by LTLAXIO1:42;
{} LTLB_WFF |- (Q ^) => H₁(g) by Th17, A4;
then {} LTLB_WFF |- 'X' ((Q ^) => H₁(f)) by A10, LTLAXIO1:47, LTLAXIO1:44;
then {} LTLB_WFF |- ('X' (Q ^)) => ('X' H₁(f)) by A11, LTLAXIO1:43;
hence {} LTLB_WFF |- (R ^) => ('X' H₁(f)) by LTLAXIO1:47, A5; :: thesis: verum

end;

now :: thesis: for i being Nat st i in dom f holds
{} LTLB_WFF |- (f /. i) => ('X' H₁(f))

let i be Nat; :: thesis: ( i in dom f implies {} LTLB_WFF |- (f /. i) => ('X' H₁(f)) )
assume i in dom f ; :: thesis: {} LTLB_WFF |- (f /. i) => ('X' H₁(f))
then f /. i in (rngr T) ^ by PARTFUN2:2, A1;
then consider R being PNPair such that
A12: f /. i = R ^ and
A13: R in rngr T ;
ex t being Node of T st
( R = T . t & t <> {} ) by A13;
then R in rng T by FUNCT_1:3;
hence {} LTLB_WFF |- (f /. i) => ('X' H₁(f)) by A2, A12; :: thesis: verum

end;

hence {} LTLB_WFF |- H₁(f) => ('X' H₁(f)) by LTLAXIO2:57; :: thesis: verum