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