let Al be QC-alphabet ; :: thesis: for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al
let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al
let P be QC-pred_symbol of k,Al; :: thesis: for ll being CQC-variable_list of k,Al
for Sub being CQC_Substitution of Al holds P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al
let ll be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al holds P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al
let Sub be CQC_Substitution of Al; :: thesis: P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al
CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub)) by Th8;
hence P ! (CQC_Subst (ll,Sub)) is Element of CQC-WFF Al ; :: thesis: verum