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