let X be Subset of LTLB_WFF; :: thesis: for f2, f, f1 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i
let f2, f, f1 be FinSequence of LTLB_WFF ; :: thesis: ( f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) implies for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i )
assume that
A1: f2 = f ^ f1 and
1 <= len f and
1 <= len f1 and
A2: for i being Nat st 1 <= i & i <= len f holds
prc f,X,i and
A3: for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ; :: thesis: for i being Nat st 1 <= i & i <= len f2 holds
prc f2,X,i
A4: len f2 = (len f) + (len f1) by A1, FINSEQ_1:22;
A5: for k being Nat st 1 <= k & k <= len f1 holds
f1 . k = f2 . (k + (len f)) by A1, FINSEQ_1:65;
let i be Nat; :: thesis: ( 1 <= i & i <= len f2 implies prc f2,X,i )
assume that
A6: 1 <= i and
A7: i <= len f2 ; :: thesis: prc f2,X,i

per cases ( i <= len f or (len f) + 1 <= i ) by NAT_1:13;

suppose A8: i <= len f ; :: thesis: prc f2,X,i

then A9: f /. i = f . i by A6, Th1
.= f2 . i by A1, A6, A8, FINSEQ_1:64
.= f2 /. i by A6, A7, Th1 ;
A10: prc f,X,i by A2, A6, A8;

per cases ( f . i in LTL_axioms or f . i in X or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ) by A10, Def30;

suppose f . i in LTL_axioms ; :: thesis: prc f2,X,i

then f2 . i in LTL_axioms by A1, A6, A8, FINSEQ_1:64;
hence prc f2,X,i by Def30; :: thesis: verum

end;

suppose f . i in X ; :: thesis: prc f2,X,i

then f2 . i in X by A1, A6, A8, FINSEQ_1:64;
hence prc f2,X,i by Def30; :: thesis: verum

end;

suppose ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ) ; :: thesis: prc f2,X,i

then consider j, k being Nat such that
A11: 1 <= j and
A12: j < i and
A13: 1 <= k and
A14: k < i and
A15: ( f /. j,f /. k MP_rule f /. i or f /. j,f /. k IND_rule f /. i ) ;
A16: k <= len f by A8, A14, XXREAL_0:2;
then A17: k <= len f2 by A4, NAT_1:12;
A18: f /. k = f . k by A13, A16, Th1
.= f2 . k by A1, A13, A16, FINSEQ_1:64
.= f2 /. k by A13, A17, Th1 ;
A19: j <= len f by A8, A12, XXREAL_0:2;
then A20: j <= len f2 by A4, NAT_1:12;
f /. j = f . j by A11, A19, Th1
.= f2 . j by A1, A11, A19, FINSEQ_1:64
.= f2 /. j by A11, A20, Th1 ;
hence prc f2,X,i by A9, A11, A12, A13, A14, A15, A18, Def30; :: thesis: verum

end;

suppose ex j being Nat st
( 1 <= j & j < i & f /. j NEX_rule f /. i ) ; :: thesis: prc f2,X,i

then consider j being Nat such that
A21: 1 <= j and
A22: j < i and
A23: f /. j NEX_rule f /. i ;
A24: j <= len f by A8, A22, XXREAL_0:2;
then A25: j <= len f2 by A4, NAT_1:12;
f /. j = f . j by A21, A24, Th1
.= f2 . j by A1, A21, A24, FINSEQ_1:64
.= f2 /. j by A21, A25, Th1 ;
hence prc f2,X,i by A9, A21, A22, A23, Def30; :: thesis: verum

end;

end;

end;

suppose A26: (len f) + 1 <= i ; :: thesis: prc f2,X,i

set i1 = i -' (len f);
i <= (len f) + (len f1) by A1, A7, FINSEQ_1:22;
then i -' (len f) <= ((len f) + (len f1)) -' (len f) by NAT_D:42;
then A27: i -' (len f) <= len f1 by NAT_D:34;
1 <= i -' (len f) by A26, NAT_D:55;
then prc f2,X,(i -' (len f)) + (len f) by A3, A4, A5, A27, Th40;
hence prc f2,X,i by A26, NAT_D:43, NAT_D:55; :: thesis: verum

end;

end;