let X be Subset of LTLB_WFF; :: thesis: for f, f1, f2 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
prc0 f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc0 f2,X,i
let f, f1, f2 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
prc0 f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) implies for i being Nat st 1 <= i & i <= len f2 holds
prc0 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
prc0 f,X,i and
A3: for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ; :: thesis: for i being Nat st 1 <= i & i <= len f2 holds
prc0 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 prc0 f2,X,i )
assume that
A6: 1 <= i and
A7: i <= len f2 ; :: thesis: prc0 f2,X,i

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

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

then A9: f /. i = f . i by A6, Lm1
.= f2 . i by A1, A6, A8, FINSEQ_1:64
.= f2 /. i by A6, A7, Lm1 ;

per cases ( f . i in LTL0_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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) by A2, A6, A8, Def29;

suppose f . i in LTL0_axioms ; :: thesis: prc0 f2,X,i

hence prc0 f2,X,i by A1, A6, A8, FINSEQ_1:64; :: thesis: verum

end;

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

hence prc0 f2,X,i by A1, A6, A8, FINSEQ_1:64; :: 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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) ; :: thesis: prc0 f2,X,i

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

end;

suppose ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ; :: thesis: prc0 f2,X,i

then consider j being Nat such that
A20: 1 <= j and
A21: j < i and
A22: ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ;
A23: j <= len f by A8, A21, XXREAL_0:2;
then A24: j <= len f2 by A4, NAT_1:12;
f /. j = f . j by A20, A23, Lm1
.= f2 . j by A1, A20, A23, FINSEQ_1:64
.= f2 /. j by A20, A24, Lm1 ;
hence prc0 f2,X,i by A9, A20, A21, A22; :: thesis: verum

end;

end;

end;

suppose A25: (len f) + 1 <= i ; :: thesis: prc0 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 A26: i -' (len f) <= len f1 by NAT_D:34;
1 <= i -' (len f) by A25, NAT_D:55;
then prc0 f2,X,(i -' (len f)) + (len f) by A3, A4, A5, A26, Th38;
hence prc0 f2,X,i by A25, NAT_D:43, NAT_D:55; :: thesis: verum

end;

end;