take L = {} ; :: thesis: ( L is CQC_Substitution of A & L is finite )
L is PartFunc of (bound_QC-variables A),(bound_QC-variables A) by RELSET_1:12;
hence L is CQC_Substitution of A by PARTFUN1:45; :: thesis: L is finite
thus L is finite ; :: thesis: verum