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