let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for X being Subset of (CQC-WFF Al) st p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } & not x in still_not-bound_in p holds
p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }
let p, q be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al
for X being Subset of (CQC-WFF Al) st p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } & not x in still_not-bound_in p holds
p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }
let x be bound_QC-variable of Al; :: thesis: for X being Subset of (CQC-WFF Al) st p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } & not x in still_not-bound_in p holds
p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }
let X be Subset of (CQC-WFF Al); :: thesis: ( p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } & not x in still_not-bound_in p implies p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) } )
assume that
A1: p => q in { F where F is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } and
A2: not x in still_not-bound_in p ; :: thesis: p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }
ex t being Element of CQC-WFF Al st
( t = p => q & ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = t ) ) by A1;
then consider f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] such that
A3: f is_a_proof_wrt X and
A4: Effect f = p => q ;
reconsider qq = [(p => (All (x,q))),8] as Element of [:(CQC-WFF Al),Proof_Step_Kinds:] by Th17, ZFMISC_1:87;
set h = f ^ <*qq*>;
A5: len (f ^ <*qq*>) = (len f) + (len <*qq*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
for n being Nat st 1 <= n & n <= len (f ^ <*qq*>) holds
f ^ <*qq*>,n is_a_correct_step_wrt X

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len (f ^ <*qq*>) implies f ^ <*qq*>,n is_a_correct_step_wrt X )
assume that
A6: 1 <= n and
A7: n <= len (f ^ <*qq*>) ; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

now :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

per cases ( n <= len f or n = len (f ^ <*qq*>) ) by A5, A7, NAT_1:8;

suppose A8: n <= len f ; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

then f,n is_a_correct_step_wrt X by A3, A6;
hence f ^ <*qq*>,n is_a_correct_step_wrt X by A6, A8, Th23; :: thesis: verum

end;

suppose A9: n = len (f ^ <*qq*>) ; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

then (f ^ <*qq*>) . n = qq by A5, FINSEQ_1:42;
then A10: ( ((f ^ <*qq*>) . n) `2 = 8 & ((f ^ <*qq*>) . n) `1 = p => (All (x,q)) ) ;
len f <> 0 by A3;
then len f in Seg (len f) by FINSEQ_1:3;
then len f in dom f by FINSEQ_1:def 3;
then A11: ((f ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by FINSEQ_1:def 7
.= p => q by A4, A3, Def6 ;
A12: 1 <= len f by A3, Th21;
len f < n by A5, A9, NAT_1:13;
hence f ^ <*qq*>,n is_a_correct_step_wrt X by A2, A10, A11, A12, Def4; :: thesis: verum

end;

end;

end;

hence f ^ <*qq*>,n is_a_correct_step_wrt X ; :: thesis: verum

end;

then A13: f ^ <*qq*> is_a_proof_wrt X ;
Effect (f ^ <*qq*>) = ((f ^ <*qq*>) . ((len f) + 1)) `1 by A5, Def6
.= qq `1 by FINSEQ_1:42
.= p => (All (x,q)) ;
hence p => (All (x,q)) in { G where G is Element of CQC-WFF Al : ex f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) } by A13; :: thesis: verum