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 (Sub_P (P,ll,Sub)) `1 = P ! ll
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 (Sub_P (P,ll,Sub)) `1 = P ! ll
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 (Sub_P (P,ll,Sub)) `1 = P ! ll
let ll be CQC-variable_list of k,Al; :: thesis: for Sub being CQC_Substitution of Al holds (Sub_P (P,ll,Sub)) `1 = P ! ll
let Sub be CQC_Substitution of Al; :: thesis: (Sub_P (P,ll,Sub)) `1 = P ! ll
Sub_P (P,ll,Sub) = [(P ! ll),Sub] by SUBSTUT1:9;
hence (Sub_P (P,ll,Sub)) `1 = P ! ll ; :: thesis: verum