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