let Al be QC-alphabet ; :: thesis: for S being Element of CQC-Sub-WFF Al st S is Sub_atomic holds
CQC_Sub S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2)))
let S be Element of CQC-Sub-WFF Al; :: thesis: ( S is Sub_atomic implies CQC_Sub S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) )
ex F being Function of (QC-Sub-WFF Al),(QC-WFF Al) st
( CQC_Sub S = F . S & ( for S9 being Element of QC-Sub-WFF Al holds
( ( S9 is Al -Sub_VERUM implies F . S9 = VERUM Al ) & ( 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 SUBSTUT1:def 38;
hence ( S is Sub_atomic implies CQC_Sub S = (the_pred_symbol_of (S `1)) ! (CQC_Subst ((Sub_the_arguments_of S),(S `2))) ) ; :: thesis: verum