let a be set ; :: thesis: for Sub being CQC_Substitution st a in dom Sub holds
Sub . a in bound_QC-variables
let Sub be CQC_Substitution; :: thesis: ( a in dom Sub implies Sub . a in bound_QC-variables )
assume a in dom Sub ; :: thesis: Sub . a in bound_QC-variables
then a in dom (@ Sub) ;
hence Sub . a in bound_QC-variables by PARTFUN1:4; :: thesis: verum