let s be QC-formula; :: thesis: for x, y being bound_QC-variable
for X being Subset of CQC-WFF st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } holds
s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }
let x, y be bound_QC-variable; :: thesis: for X being Subset of CQC-WFF st s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } holds
s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }
let X be Subset of CQC-WFF; :: thesis: ( s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } implies s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) } )
assume that
A1: ( s . x in CQC-WFF & s . y in CQC-WFF ) and
A2: not x in still_not-bound_in s and
A3: s . x in { F where F is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = F ) } ; :: thesis: s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) }
ex t being Element of CQC-WFF st
( t = s . x & ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = t ) ) by A3;
then consider f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] such that
A5: f is_a_proof_wrt X and
A6: Effect f = s . x ;
A7: f <> {} by A5, Def5;
reconsider qq = [(s . y),9] as Element of [:CQC-WFF,Proof_Step_Kinds:] by A1, Th43, ZFMISC_1:106;
set h = f ^ <*qq*>;
A8: len (f ^ <*qq*>) = (len f) + (len <*qq*>) by FINSEQ_1:35
.= (len f) + 1 by FINSEQ_1:56 ;
for n being Element of NAT st 1 <= n & n <= len (f ^ <*qq*>) holds
f ^ <*qq*>,n is_a_correct_step_wrt X

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (f ^ <*qq*>) implies f ^ <*qq*>,n is_a_correct_step_wrt X )
assume that
A10: 1 <= n and
A11: n <= len (f ^ <*qq*>) ; :: thesis: f ^ <*qq*>,n is_a_correct_step_wrt X

now

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

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

then f,n is_a_correct_step_wrt X by A5, A10, Def5;
hence f ^ <*qq*>,n is_a_correct_step_wrt X by A10, A13, Th60; :: thesis: verum

end;

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

then (f ^ <*qq*>) . n = qq by A8, FINSEQ_1:59;
then A17: ( ((f ^ <*qq*>) . n) `2 = 9 & ((f ^ <*qq*>) . n) `1 = s . y ) by MCART_1:7;
len f <> 0 by A5, Th58;
then len f in Seg (len f) by FINSEQ_1:5;
then len f in dom f by FINSEQ_1:def 3;
then A21: ((f ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by FINSEQ_1:def 7
.= s . x by A6, A7, Def6 ;
A22: 1 <= len f by A5, Th58;
len f < n by A8, A15, NAT_1:13;
hence f ^ <*qq*>,n is_a_correct_step_wrt X by A1, A2, A17, A21, A22, Def4; :: thesis: verum

end;

end;

end;

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

end;

then A24: f ^ <*qq*> is_a_proof_wrt X by Def5;
Effect (f ^ <*qq*>) = ((f ^ <*qq*>) . ((len f) + 1)) `1 by A8, Def6
.= qq `1 by FINSEQ_1:59
.= s . y by MCART_1:7 ;
hence s . y in { G where G is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st
( f is_a_proof_wrt X & Effect f = G ) } by A24; :: thesis: verum