let F be Subset of PL-WFF; :: thesis: for f, f1, f2 being FinSequence of PL-WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc f2,F,i
let f, f1, f2 be FinSequence of PL-WFF ; :: thesis: ( f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ) implies for i being Nat st 1 <= i & i <= len f2 holds
prc f2,F,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,F,i and
A3: for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ; :: thesis: for i being Nat st 1 <= i & i <= len f2 holds
prc f2,F,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,F,i )
assume that
A6: 1 <= i and
A7: i <= len f2 ; :: thesis: prc f2,F,i
per cases ( i <= len f or (len f) + 1 <= i ) by NAT_1:13;
suppose A8: i <= len f ; :: thesis: prc f2,F,i
then A9: f /. i = f . i by A6, LTLAXIO5:1
.= f2 . i by A1, A6, A8, FINSEQ_1:64
.= f2 /. i by A6, A7, LTLAXIO5:1 ;
per cases ( f . i in PL_axioms or f . i in F or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) ) by A2, A6, A8, defprc;
suppose f . i in PL_axioms ; :: thesis: prc f2,F,i
hence prc f2,F,i by A1, A6, A8, FINSEQ_1:64; :: thesis: verum
end;
suppose f . i in F ; :: thesis: prc f2,F,i
hence prc f2,F,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 ) ; :: thesis: prc f2,F,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 ;
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, LTLAXIO5:1
.= f2 . k by A1, A12, A15, FINSEQ_1:64
.= f2 /. k by A12, A16, LTLAXIO5:1 ;
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, LTLAXIO5:1
.= f2 . j by A1, A10, A18, FINSEQ_1:64
.= f2 /. j by A10, A19, LTLAXIO5:1 ;
hence prc f2,F,i by A9, A10, A11, A12, A13, A14, A17; :: thesis: verum
end;
end;
end;
suppose A25: (len f) + 1 <= i ; :: thesis: prc f2,F,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 prc f2,F,(i -' (len f)) + (len f) by A3, A4, A5, A26, Th38;
hence prc f2,F,i by A25, NAT_D:43, NAT_D:55; :: thesis: verum
end;
end;