let p be Element of CQC-WFF ; :: thesis: for x being bound_QC-variable
for f being FinSequence of CQC-WFF st ex y being bound_QC-variable st |- f ^ <*(p . x,y)*> holds
|- f ^ <*(Ex x,p)*>
let x be bound_QC-variable; :: thesis: for f being FinSequence of CQC-WFF st ex y being bound_QC-variable st |- f ^ <*(p . x,y)*> holds
|- f ^ <*(Ex x,p)*>
let f be FinSequence of CQC-WFF ; :: thesis: ( ex y being bound_QC-variable st |- f ^ <*(p . x,y)*> implies |- f ^ <*(Ex x,p)*> )
given y being bound_QC-variable such that A1: |- f ^ <*(p . x,y)*> ; :: thesis: |- f ^ <*(Ex x,p)*>
set f1 = (f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>;
A2: Ant ((f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>) = f ^ <*(All x,('not' p))*> by Th5;
(len f) + 1 = (len f) + (len <*(All x,('not' p))*>) by FINSEQ_1:56;
then (len f) + 1 = len (Ant ((f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>)) by A2, FINSEQ_1:35;
then A3: (len f) + 1 in dom (Ant ((f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>)) by A2, Th10;
A4: Suc ((f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>) = All x,('not' p) by Th5;
(Ant ((f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>)) . ((len f) + 1) = All x,('not' p) by A2, FINSEQ_1:59;
then Suc ((f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>) is_tail_of Ant ((f ^ <*(All x,('not' p))*>) ^ <*(All x,('not' p))*>) by A4, A3, Def3;
then |- (f ^ <*(All x,('not' p))*>) ^ <*(('not' p) . x,y)*> by A2, A4, Th33, Th42;
then |- (f ^ <*(All x,('not' p))*>) ^ <*('not' (p . x,y))*> by Th57;
then |- (f ^ <*(p . x,y)*>) ^ <*('not' (All x,('not' p)))*> by Th49;
then A5: |- (f ^ <*(p . x,y)*>) ^ <*(Ex x,p)*> by QC_LANG2:def 5;
1 <= len (f ^ <*(p . x,y)*>) by Th10;
then |- (Ant (f ^ <*(p . x,y)*>)) ^ <*(Ex x,p)*> by A1, A5, Th45;
hence |- f ^ <*(Ex x,p)*> by Th5; :: thesis: verum