let A, B be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |-0 A & F |-0 A => B holds
F |-0 B

let F be Subset of LTLB_WFF; :: thesis: ( F |-0 A & F |-0 A => B implies F |-0 B )
assume that
A1: F |-0 A and
A2: F |-0 A => B ; :: thesis: F |-0 B
consider f being FinSequence of LTLB_WFF such that
A3: f . (len f) = A and
A4: 1 <= len f and
A5: for i being Nat st 1 <= i & i <= len f holds
prc0 f,F,i by A1;
consider g being FinSequence of LTLB_WFF such that
A6: g . (len g) = A => B and
A7: 1 <= len g and
A8: for i being Nat st 1 <= i & i <= len g holds
prc0 g,F,i by A2;
A9: for i being Nat st 1 <= i & i <= len (f ^ g) holds
prc0 f ^ g,F,i by A4, A5, A7, A8, Th39;
set h = (f ^ g) ^ <*B*>;
A10: (f ^ g) ^ <*B*> = f ^ (g ^ <*B*>) by FINSEQ_1:32;
A11: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
then A12: 1 <= len (f ^ g) by ;
A13: len ((f ^ g) ^ <*B*>) = (len (f ^ g)) + () by FINSEQ_1:22
.= (len (f ^ g)) + 1 by FINSEQ_1:39 ;
then 1 <= len ((f ^ g) ^ <*B*>) by ;
then A14: ((f ^ g) ^ <*B*>) /. (len ((f ^ g) ^ <*B*>)) = ((f ^ g) ^ <*B*>) . (len ((f ^ g) ^ <*B*>)) by Lm1
.= B by ;
len ((f ^ g) ^ <*B*>) = (len f) + ((len g) + 1) by ;
then A15: len f < len ((f ^ g) ^ <*B*>) by NAT_1:16;
then A16: ((f ^ g) ^ <*B*>) /. (len f) = ((f ^ g) ^ <*B*>) . (len f) by
.= A by ;
A17: len (f ^ g) < len ((f ^ g) ^ <*B*>) by ;
then ((f ^ g) ^ <*B*>) /. (len (f ^ g)) = ((f ^ g) ^ <*B*>) . (len (f ^ g)) by
.= (f ^ g) . (len (f ^ g)) by
.= (f ^ g) . ((len f) + (len g)) by FINSEQ_1:22
.= A => B by ;
then ((f ^ g) ^ <*B*>) /. (len f),((f ^ g) ^ <*B*>) /. (len (f ^ g)) MP_rule ((f ^ g) ^ <*B*>) /. (len ((f ^ g) ^ <*B*>)) by ;
then prc0 (f ^ g) ^ <*B*>,F, len ((f ^ g) ^ <*B*>) by A4, A12, A15, A17;
hence F |-0 B by ; :: thesis: verum