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