let Al be QC-alphabet ; :: thesis: for s being QC-formula of Al
for x, y being bound_QC-variable of Al
for X being Subset of (CQC-WFF Al) st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
holds
s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}

let s be QC-formula of Al; :: thesis: for x, y being bound_QC-variable of Al
for X being Subset of (CQC-WFF Al) st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
holds
s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}

let x, y be bound_QC-variable of Al; :: thesis: for X being Subset of (CQC-WFF Al) st s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
holds
s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}

let X be Subset of (CQC-WFF Al); :: thesis: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
implies s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}
)

assume that
A1: ( s . x in CQC-WFF Al & s . y in CQC-WFF Al ) and
A2: not x in still_not-bound_in s and
A3: s . x in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
; :: thesis: s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}

ex t being Element of CQC-WFF Al st
( t = s . x & ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = t ) ) by A3;
then consider f being FinSequence of such that
A4: f is_a_proof_wrt X and
A5: Effect f = s . x ;
reconsider qq = [(s . y),9] as Element of by ;
set h = f ^ <*qq*>;
A6: 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
A7: 1 <= n and
A8: n <= len (f ^ <*qq*>) ; :: thesis:
now :: thesis:
per cases ( n <= len f or n = len (f ^ <*qq*>) ) by ;
suppose A10: n = len (f ^ <*qq*>) ; :: thesis:
then (f ^ <*qq*>) . n = qq by ;
then A11: ( ((f ^ <*qq*>) . n) `2 = 9 & ((f ^ <*qq*>) . n) `1 = s . y ) ;
len f <> 0 by A4;
then len f in Seg (len f) by FINSEQ_1:3;
then len f in dom f by FINSEQ_1:def 3;
then A12: ((f ^ <*qq*>) . (len f)) `1 = (f . (len f)) `1 by FINSEQ_1:def 7
.= s . x by A5, A4, Def6 ;
A13: 1 <= len f by ;
len f < n by ;
hence f ^ <*qq*>,n is_a_correct_step_wrt X by A1, A2, A11, A12, A13, Def4; :: thesis: verum
end;
end;
end;
hence f ^ <*qq*>,n is_a_correct_step_wrt X ; :: thesis: verum
end;
then A14: f ^ <*qq*> is_a_proof_wrt X ;
Effect (f ^ <*qq*>) = ((f ^ <*qq*>) . ((len f) + 1)) `1 by
.= qq `1 by FINSEQ_1:42
.= s . y ;
hence s . y in { G where G is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = G )
}
by A14; :: thesis: verum