let S be Element of CQC-Sub-WFF ; :: 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 ,QC-WFF st
( CQC_Sub S = F . S & ( 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 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