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 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 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:1;
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 A

proof

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

now :: thesis: ( ( (@ l) . x in dom Sub & (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A ) or ( not (@ l) . x in dom Sub & (CQC_Subst ((@ l),Sub)) . x in bound_QC-variables A ) )

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 A

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

end;

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

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

end;

end;

end;

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

end;

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