let F be Subset of PL-WFF; 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 ; ( 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
; 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; ( 1 <= i & i <= len f2 implies prc f2,F,i )
assume that
A6:
1 <= i
and
A7:
i <= len f2
; prc f2,F,i
per cases
( i <= len f or (len f) + 1 <= i )
by NAT_1:13;
suppose A8:
i <= len f
;
prc f2,F,ithen 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
ex
j,
k being
Nat st
( 1
<= j &
j < i & 1
<= k &
k < i &
f /. j,
f /. k MP_rule f /. i )
;
prc f2,F,ithen 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;
verum end; end; end; suppose A25:
(len f) + 1
<= i
;
prc f2,F,iset 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;
verum end; end;