let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of
for Sub being CQC_Substitution holds CQC_Sub (Sub_P P,ll,Sub) = P ! (CQC_Subst ll,Sub)
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of
for Sub being CQC_Substitution holds CQC_Sub (Sub_P P,ll,Sub) = P ! (CQC_Subst ll,Sub)
let ll be CQC-variable_list of ; :: thesis: for Sub being CQC_Substitution holds CQC_Sub (Sub_P P,ll,Sub) = P ! (CQC_Subst ll,Sub)
let Sub be CQC_Substitution; :: thesis: CQC_Sub (Sub_P P,ll,Sub) = P ! (CQC_Subst ll,Sub)
reconsider P' = P as QC-pred_symbol ;
A1: Sub_P P,ll,Sub = [(P ! ll),Sub] by SUBSTUT1:9;
then A2: (Sub_P P,ll,Sub) `1 = P ! ll by MCART_1:7;
A3: (Sub_P P,ll,Sub) `2 = Sub by A1, MCART_1:7;
P ! ll is atomic by QC_LANG1:def 17;
then ( P' ! ll = P ! ll & Sub_the_arguments_of (Sub_P P,ll,Sub) = ll & the_pred_symbol_of ((Sub_P P,ll,Sub) `1 ) = P ) by A2, QC_LANG1:def 21, SUBSTUT1:def 29;
hence CQC_Sub (Sub_P P,ll,Sub) = P ! (CQC_Subst ll,Sub) by A3, Th6; :: thesis: verum