let p be Element of LTLB_WFF ; :: thesis: 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
prc0 f1,X,i ) & prc0 f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & X |-0 p )

let X be Subset of LTLB_WFF; :: thesis: 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
prc0 f1,X,i ) & prc0 f,X, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & X |-0 p )

let f, f1 be FinSequence of LTLB_WFF ; :: thesis: ( f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) & prc0 f,X, len f implies ( ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & X |-0 p ) )

assume that
A1: f = f1 ^ <*p*> and
1 <= len f1 and
A2: for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ; :: thesis: ( not prc0 f,X, len f or ( ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & X |-0 p ) )

A3: len f = (len f1) + () by
.= (len f1) + 1 by FINSEQ_1:39 ;
assume A4: prc0 f,X, len f ; :: thesis: ( ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & X |-0 p )

A5: 0 + (len f1) <= len f by ;
A6: now :: thesis: for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies prc0 f,X,b1 )
assume that
A7: 1 <= i and
A8: i <= len f ; :: thesis: prc0 f,X,b1
A9: ( i < (len f1) + 1 or i = (len f1) + 1 ) by ;
A10: for k being Nat st 1 <= k & k <= len f1 holds
f1 . k = f . (k + 0) by ;
per cases ( i <= len f1 or i = len f ) by ;
suppose i <= len f1 ; :: thesis: prc0 f,X,b1
then prc0 f,X,i + 0 by A2, A5, A7, A10, Th38;
hence prc0 f,X,i ; :: thesis: verum
end;
suppose i = len f ; :: thesis: prc0 f,X,b1
hence prc0 f,X,i by A4; :: thesis: verum
end;
end;
end;
hence for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ; :: thesis: X |-0 p
f . (len f) = f . ((len f1) + ()) by
.= f . ((len f1) + 1) by FINSEQ_1:39
.= p by ;
hence X |-0 p by ; :: thesis: verum