let p be Element of LTLB_WFF ; for X being Subset of LTLB_WFF
for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
let X be Subset of LTLB_WFF; for f, f1 being FinSequence of LTLB_WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
let f, f1 be FinSequence of LTLB_WFF ; ( f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i ) & prc f,X, len f implies ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p ) )
assume that
A1:
f = f1 ^ <*p*>
and
1 <= len f1
and
A2:
for i being Nat st 1 <= i & i <= len f1 holds
prc f1,X,i
; ( not prc f,X, len f or ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p ) )
A3: len f =
(len f1) + (len <*p*>)
by A1, FINSEQ_1:22
.=
(len f1) + 1
by FINSEQ_1:39
;
assume A4:
prc f,X, len f
; ( ( for i being Nat st 1 <= i & i <= len f holds
prc f,X,i ) & X |- p )
A5:
0 + (len f1) <= len f
by A3, NAT_1:12;
hence
for i being Nat st 1 <= i & i <= len f holds
prc f,X,i
; X |- p
f . (len f) =
f . ((len f1) + (len <*p*>))
by A1, FINSEQ_1:22
.=
f . ((len f1) + 1)
by FINSEQ_1:39
.=
p
by A1, FINSEQ_1:42
;
hence
X |- p
by A3, XREAL_1:31, A6; verum