let S be Element of QC-Sub-WFF ; :: thesis: ( S is Sub_conjunctive implies CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) )
consider F being Function of QC-Sub-WFF ,QC-WFF such that
A1: CQC_Sub S = F . S and
A2: 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;
consider F1 being Function of QC-Sub-WFF ,QC-WFF such that
A3: CQC_Sub (Sub_the_left_argument_of S) = F1 . (Sub_the_left_argument_of S) and
A4: for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F1 . S' = VERUM ) & ( S' is Sub_atomic implies F1 . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F1 . S' = 'not' (F1 . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F1 . S' = (F1 . (Sub_the_left_argument_of S')) '&' (F1 . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F1 . S' = Quant S',(F1 . (Sub_the_scope_of S')) ) ) by Def38;
consider F2 being Function of QC-Sub-WFF ,QC-WFF such that
A5: CQC_Sub (Sub_the_right_argument_of S) = F2 . (Sub_the_right_argument_of S) and
A6: for S' being Element of QC-Sub-WFF holds
( ( S' is Sub_VERUM implies F2 . S' = VERUM ) & ( S' is Sub_atomic implies F2 . S' = (the_pred_symbol_of (S' `1 )) ! (CQC_Subst (Sub_the_arguments_of S'),(S' `2 )) ) & ( S' is Sub_negative implies F2 . S' = 'not' (F2 . (Sub_the_argument_of S')) ) & ( S' is Sub_conjunctive implies F2 . S' = (F2 . (Sub_the_left_argument_of S')) '&' (F2 . (Sub_the_right_argument_of S')) ) & ( S' is Sub_universal implies F2 . S' = Quant S',(F2 . (Sub_the_scope_of S')) ) ) by Def38;
( F1 = F & F2 = F ) by A2, A4, A6, Lm5;
hence ( S is Sub_conjunctive implies CQC_Sub S = (CQC_Sub (Sub_the_left_argument_of S)) '&' (CQC_Sub (Sub_the_right_argument_of S)) ) by A1, A2, A3, A5; :: thesis: verum