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;

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

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

hence
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,b_{1} )

assume that

A7: 1 <= i and

A8: i <= len f ; :: thesis: prc0 f,X,b_{1}

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;

end;assume that

A7: 1 <= i and

A8: i <= len f ; :: thesis: prc0 f,X,b

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;

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