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 ;
A5: for k being Nat st 1 <= k & k <= len f1 holds
f1 . k = f2 . (k + (len f)) by ;
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
.= f2 . i by
.= 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 ; :: thesis: verum
end;
suppose f . i in X ; :: thesis: prc0 f2,X,i
hence prc0 f2,X,i by ; :: 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 ;
then A16: k <= len f2 by ;
A17: f /. k = f . k by
.= f2 . k by
.= f2 /. k by ;
A18: j <= len f by ;
then A19: j <= len f2 by ;
f /. j = f . j by
.= f2 . j by
.= f2 /. j by ;
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 ;
then A24: j <= len f2 by ;
f /. j = f . j by
.= f2 . j by
.= f2 /. j by ;
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 ;
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 ;
then prc0 f2,X,(i -' (len f)) + (len f) by A3, A4, A5, A26, Th38;
hence prc0 f2,X,i by ; :: thesis: verum
end;
end;