let f, f1 be FinSequence of LTLB_WFF ; :: thesis: ( rng f c= rng f1 implies ('not' ((con (nega f)) /. (len (con (nega f))))) => ('not' ((con (nega f1)) /. (len (con (nega f1))))) is ctaut )
assume A1: rng f c= rng f1 ; :: thesis: ('not' ((con (nega f)) /. (len (con (nega f))))) => ('not' ((con (nega f1)) /. (len (con (nega f1))))) is ctaut
set p = H₁(f) => H₁(f1);
assume not H₁(f) => H₁(f1) is ctaut ; :: thesis: contradiction
then consider g being Function of LTLB_WFF,BOOLEAN such that
A2: not (VAL g) . (H₁(f) => H₁(f1)) = 1 ;
set v = VAL g;
(VAL g) . (H₁(f) => H₁(f1)) = 0 by A2, XBOOLEAN:def 3;
then A3: ((VAL g) . H₁(f)) => ((VAL g) . H₁(f1)) = 0 by LTLAXIO1:def 15;
A4: ( (VAL g) . H₁(f) = TRUE or (VAL g) . H₁(f) = FALSE ) by XBOOLEAN:def 3;

now :: 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 )
assume A5: i in dom f ; :: thesis: (VAL g) . (f /. i) = 0
then f . i in rng f by FUNCT_1:3;
then consider j being object such that
A6: j in dom f1 and
A7: f . i = f1 . j by A1, FUNCT_1:def 3;
f1 /. j = f1 . j by PARTFUN1:def 6, A6
.= f /. i by A5, PARTFUN1:def 6, A7 ;
hence (VAL g) . (f /. i) = 0 by A6, Th20, A3, A4; :: thesis: verum
reconsider j = j as Nat by A6;

end;

hence contradiction by A3, A4, Th20; :: thesis: verum