len (CQC_Subst (@ l),Sub) = len (@ l) by Def3;
then A1: dom (CQC_Subst (@ l),Sub) = Seg (len (@ l)) by FINSEQ_1:def 3;
A2: for k being Element of NAT st k in Seg (len (@ l)) holds
( ( (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = (@ l) . k ) )

proof

let k be Element of NAT ; :: thesis: ( k in Seg (len (@ l)) implies ( ( (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = (@ l) . k ) ) )
assume k in Seg (len (@ l)) ; :: thesis: ( ( (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = (@ l) . k ) )
then ( 1 <= k & k <= len (@ l) ) by FINSEQ_1:3;
hence ( ( (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = Sub . ((@ l) . k) ) & ( not (@ l) . k in dom Sub implies (CQC_Subst (@ l),Sub) . k = (@ l) . k ) ) by Def3; :: thesis: verum

end;

rng (CQC_Subst (@ l),Sub) c= bound_QC-variables

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (CQC_Subst (@ l),Sub) or y in bound_QC-variables )
assume y in rng (CQC_Subst (@ l),Sub) ; :: thesis: y in bound_QC-variables
then consider x being set such that
A3: x in dom (CQC_Subst (@ l),Sub) and
A4: (CQC_Subst (@ l),Sub) . x = y by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;

now

per cases ( (@ l) . x in dom Sub or not (@ l) . x in dom Sub ) ;

case A5: (@ l) . x in dom Sub ; :: thesis: (CQC_Subst (@ l),Sub) . x in bound_QC-variables

then (CQC_Subst (@ l),Sub) . x = Sub . ((@ l) . x) by A1, A2, A3;
hence (CQC_Subst (@ l),Sub) . x in bound_QC-variables by A5, Th1; :: thesis: verum

end;

case A6: not (@ l) . x in dom Sub ; :: thesis: (CQC_Subst (@ l),Sub) . x in bound_QC-variables

A7: rng l c= bound_QC-variables ;
x in dom (@ l) by A1, A3, FINSEQ_1:def 3;
then A8: (@ l) . x in rng (@ l) by FUNCT_1:12;
(CQC_Subst (@ l),Sub) . x = (@ l) . x by A1, A2, A3, A6;
hence (CQC_Subst (@ l),Sub) . x in bound_QC-variables by A8, A7; :: thesis: verum

end;

end;

end;

hence y in bound_QC-variables by A4; :: thesis: verum

end;

hence CQC_Subst (@ l),Sub is FinSequence of bound_QC-variables by FINSEQ_1:def 4; :: thesis: verum