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) + (len <*p*>) by A1, FINSEQ_1:22
.= (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 A3, NAT_1:12;
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 A3, A8, XXREAL_0:1;
A10: for k being Nat st 1 <= k & k <= len f1 holds
f1 . k = f . (k + 0) by A1, FINSEQ_1:64;
per cases ( i <= len f1 or i = len f ) by A3, A9, NAT_1:13;
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) + (len <*p*>)) by A1, FINSEQ_1:22
.= f . ((len f1) + 1) by FINSEQ_1:39
.= p by A1, FINSEQ_1:42 ;
hence X |-0 p by A3, XREAL_1:31, A6; :: thesis: verum