let A be Element of LTLB_WFF ; :: thesis: for P being PNPair st A in rng (P `2) holds
{} LTLB_WFF |- (P ^) => ()

let P be PNPair; :: thesis: ( A in rng (P `2) implies {} LTLB_WFF |- (P ^) => () )
set fp = P `1 ;
set fm = P `2 ;
set nfm = nega (P `2);
assume A in rng (P `2) ; :: thesis: {} LTLB_WFF |- (P ^) => ()
then consider i being Nat such that
A1: i in dom (P `2) and
A2: (P `2) . i = A by FINSEQ_2:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i <= len (P `2) by ;
then A3: i <= len (nega (P `2)) by LTLAXIO2:def 4;
1 <= i by ;
then A4: i in dom (nega (P `2)) by ;
(P ^) => () is ctaut
proof
let g be Function of LTLB_WFF,BOOLEAN; :: according to LTLAXIO1:def 16 :: thesis: (VAL g) . ((P ^) => ()) = 1
set v = VAL g;
set p = (VAL g) . H2(P `1 );
set q = (VAL g) . H2( nega (P `2));
set r = (VAL g) . H2((nega (P `2)) | (i -' 1));
set s = (VAL g) . H2((nega (P `2)) /^ i);
A5: ( (VAL g) . () = 1 or (VAL g) . () = 0 ) by XBOOLEAN:def 3;
A6: (VAL g) . H2( nega (P `2)) = (((VAL g) . H2((nega (P `2)) | (i -' 1))) '&' ((VAL g) . ((nega (P `2)) /. i))) '&' ((VAL g) . H2((nega (P `2)) /^ i)) by
.= (((VAL g) . H2((nega (P `2)) | (i -' 1))) '&' ((VAL g) . ('not' ((P `2) /. i)))) '&' ((VAL g) . H2((nega (P `2)) /^ i)) by
.= (((VAL g) . H2((nega (P `2)) | (i -' 1))) '&' ((VAL g) . ())) '&' ((VAL g) . H2((nega (P `2)) /^ i)) by ;
thus (VAL g) . ((P ^) => ()) = ((VAL g) . (P ^)) => ((VAL g) . ()) by LTLAXIO1:def 15
.= (((VAL g) . H2(P `1 )) '&' ((VAL g) . H2( nega (P `2)))) => ((VAL g) . ()) by LTLAXIO1:31
.= 1 by A5, A6 ; :: thesis: verum
end;
then (P ^) => () in LTL_axioms by LTLAXIO1:def 17;
hence {} LTLB_WFF |- (P ^) => () by LTLAXIO1:42; :: thesis: verum