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