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 CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))
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 CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))
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 CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))
let ll be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al holds CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))
let Sub be CQC_Substitution of Al; :: thesis: CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub))
A1: P ! ll is atomic by QC_LANG1:def 18;
A2: Sub_P (P,ll,Sub) = [(P ! ll),Sub] by SUBSTUT1:9;
then A3: (Sub_P (P,ll,Sub)) `2 = Sub ;
(Sub_P (P,ll,Sub)) `1 = P ! ll by A2;
then ( Sub_the_arguments_of (Sub_P (P,ll,Sub)) = ll & the_pred_symbol_of ((Sub_P (P,ll,Sub)) `1) = P ) by A1, QC_LANG1:def 22, SUBSTUT1:def 29;
hence CQC_Sub (Sub_P (P,ll,Sub)) = P ! (CQC_Subst (ll,Sub)) by A3, Th6; :: thesis: verum