let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of
for e being Element of vSUB holds CQC_Sub (Sub_P P,ll,e) is Element of CQC-WFF
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of
for e being Element of vSUB holds CQC_Sub (Sub_P P,ll,e) is Element of CQC-WFF
let ll be CQC-variable_list of ; :: thesis: for e being Element of vSUB holds CQC_Sub (Sub_P P,ll,e) is Element of CQC-WFF
let e be Element of vSUB ; :: thesis: CQC_Sub (Sub_P P,ll,e) is Element of CQC-WFF
consider F being Function of QC-Sub-WFF ,QC-WFF such that
A1: ( CQC_Sub (Sub_P P,ll,e) = F . (Sub_P P,ll,e) & ( for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F . S' = VERUM ) & ( S' is Sub_atomic implies F . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F . S' = 'not' (F . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F . S' = (F . (Sub_the_left_argument_of S')) '&' (F . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F . S' = Quant S',(F . (Sub_the_scope_of S')) ) ) ) ) by Def38;
set l = Sub_the_arguments_of (Sub_P P,ll,e);
A2: Sub_the_arguments_of (Sub_P P,ll,e) is CQC-variable_list of by Def29;
then reconsider l = Sub_the_arguments_of (Sub_P P,ll,e) as FinSequence of bound_QC-variables by Th34;
reconsider s = CQC_Subst l,((Sub_P P,ll,e) `2 ) as FinSequence of bound_QC-variables ;
len l = k by A2, FINSEQ_1:def 18;
then len s = k by Def3;
then reconsider s = s as CQC-variable_list of by Th34;
Sub_P P,ll,e = [(P ! ll),e] by Th9;
then (Sub_P P,ll,e) `1 = P ! ll by MCART_1:7;
then reconsider P' = the_pred_symbol_of ((Sub_P P,ll,e) `1 ) as QC-pred_symbol of k by Lm6;
CQC_Sub (Sub_P P,ll,e) = P' ! s by A1;
hence CQC_Sub (Sub_P P,ll,e) is Element of CQC-WFF ; :: thesis: verum