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 (Sub_P (P,ll,Sub)) `1 = P ! ll
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of k
for Sub being CQC_Substitution holds (Sub_P (P,ll,Sub)) `1 = P ! ll
let ll be CQC-variable_list of k; :: thesis: for Sub being CQC_Substitution holds (Sub_P (P,ll,Sub)) `1 = P ! ll
let Sub be CQC_Substitution; :: 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 by MCART_1:7; :: thesis: verum