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