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 ex S being Element of CQC-Sub-WFF st
( S `1 = P ! ll & S `2 = Sub )
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of k
for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = P ! ll & S `2 = Sub )
let ll be CQC-variable_list of k; :: thesis: for Sub being CQC_Substitution ex S being Element of CQC-Sub-WFF st
( S `1 = P ! ll & S `2 = Sub )
let Sub be CQC_Substitution; :: thesis: ex S being Element of CQC-Sub-WFF st
( S `1 = P ! ll & S `2 = Sub )
P is QC-pred_symbol of (the_arity_of P) by QC_LANG3:3;
then k = the_arity_of P by Lm1;
then ( [(<*P*> ^ ll),Sub] in QC-Sub-WFF & len ll = the_arity_of P ) by FINSEQ_1:def 18, SUBSTUT1:def 16;
then reconsider S = [(P ! ll),Sub] as Element of QC-Sub-WFF by QC_LANG1:def 11;
take S ; :: thesis: ( S is Element of CQC-Sub-WFF & S `1 = P ! ll & S `2 = Sub )
S `1 = P ! ll by MCART_1:7;
then S in CQC-Sub-WFF by SUBSTUT1:def 39;
then reconsider S = S as Element of CQC-Sub-WFF ;
S `2 = Sub by MCART_1:7;
hence ( S is Element of CQC-Sub-WFF & S `1 = P ! ll & S `2 = Sub ) by MCART_1:7; :: thesis: verum