let p be Element of LTLB_WFF ; :: thesis: for f being FinSequence of LTLB_WFF st ( for i being Nat st i in dom f holds
{} LTLB_WFF |- p => (f /. i) ) holds
{} LTLB_WFF |- p => ((con f) /. (len (con f)))
let f be FinSequence of LTLB_WFF ; :: thesis: ( ( for i being Nat st i in dom f holds
{} LTLB_WFF |- p => (f /. i) ) implies {} LTLB_WFF |- p => ((con f) /. (len (con f))) )
assume A1: for i being Nat st i in dom f holds
{} LTLB_WFF |- p => (f /. i) ; :: thesis: {} LTLB_WFF |- p => ((con f) /. (len (con f)))

per cases ( len f = 0 or len f > 0 ) ;

suppose A2: len f = 0 ; :: thesis: {} LTLB_WFF |- p => ((con f) /. (len (con f)))

p => TVERUM is ctaut by Th22;
then A3: p => TVERUM in LTL_axioms by LTLAXIO1:def 17;
f = {} by A2;
hence {} LTLB_WFF |- p => ((con f) /. (len (con f))) by A3, Th10, LTLAXIO1:42; :: thesis: verum

end;

suppose A4: len f > 0 ; :: thesis: {} LTLB_WFF |- p => ((con f) /. (len (con f)))

defpred S₁[ Nat] means ( $1 <= len f implies {} LTLB_WFF |- p => ((con f) /. $1) );

A5: now :: thesis: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

set a = (con f) /. k;
set b = f /. (k + 1);
assume A7: k + 1 <= len f ; :: thesis: {} LTLB_WFF |- p => ((con f) /. (k + 1))
1 <= k by NAT_1:25;
then A8: (con f) /. (k + 1) = ((con f) /. k) '&&' (f /. (k + 1)) by A7, NAT_1:13, Th7;
1 <= k + 1 by NAT_1:25;
then A9: {} LTLB_WFF |- p => (f /. (k + 1)) by FINSEQ_3:25, A7, A1;
(p => ((con f) /. k)) => ((p => (f /. (k + 1))) => (p => (((con f) /. k) '&&' (f /. (k + 1))))) is ctaut by Th40;
then (p => ((con f) /. k)) => ((p => (f /. (k + 1))) => (p => (((con f) /. k) '&&' (f /. (k + 1))))) in LTL_axioms by LTLAXIO1:def 17;
then {} LTLB_WFF |- (p => ((con f) /. k)) => ((p => (f /. (k + 1))) => (p => (((con f) /. k) '&&' (f /. (k + 1))))) by LTLAXIO1:42;
then {} LTLB_WFF |- (p => (f /. (k + 1))) => (p => (((con f) /. k) '&&' (f /. (k + 1)))) by LTLAXIO1:43, A6, A7, NAT_1:13;
hence {} LTLB_WFF |- p => ((con f) /. (k + 1)) by LTLAXIO1:43, A9, A8; :: thesis: verum

end;

end;

A10: S₁[1]

proof

assume A11: 1 <= len f ; :: thesis: {} LTLB_WFF |- p => ((con f) /. 1)
then {} LTLB_WFF |- p => (f /. 1) by FINSEQ_3:25, A1;
hence {} LTLB_WFF |- p => ((con f) /. 1) by A11, Th6; :: thesis: verum

end;

A12: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A10, A5);
len f = len (con f) by A4, Def2;
hence {} LTLB_WFF |- p => H₂(f) by A12, A4; :: thesis: verum

end;

end;