let F1, F2 be Function of QC-Sub-WFF,QC-WFF; :: thesis: ( ( 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))) ) ) ) & ( 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))) ) ) ) implies F1 = F2 )
deffunc H₁( Element of QC-WFF , Element of QC-WFF ) -> Element of QC-WFF = $1 '&' $2;
deffunc H₂( Element of QC-WFF ) -> Element of QC-WFF = 'not' $1;
deffunc H₃( Element of QC-Sub-WFF ) -> Element of QC-WFF = (the_pred_symbol_of ($1 `1)) ! (CQC_Subst ((Sub_the_arguments_of $1),($1 `2)));
assume for S being Element of QC-Sub-WFF holds
( ( S is Sub_VERUM implies F1 . S = VERUM ) & ( S is Sub_atomic implies F1 . S = H₃(S) ) & ( S is Sub_negative implies F1 . S = H₂(F1 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F1 . S = H₁(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))) ) ) ; :: thesis: ( ex S being Element of QC-Sub-WFF st
( ( 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)) ) implies ( S is Sub_universal & not F2 . S = Quant (S,(F2 . (Sub_the_scope_of S))) ) ) or F1 = F2 )
then A1: for S being Element of QC-Sub-WFF
for d1, d2 being Element of QC-WFF holds
( ( S is Sub_VERUM implies F1 . S = VERUM ) & ( S is Sub_atomic implies F1 . S = H₃(S) ) & ( S is Sub_negative & d1 = F1 . (Sub_the_argument_of S) implies F1 . S = H₂(d1) ) & ( S is Sub_conjunctive & d1 = F1 . (Sub_the_left_argument_of S) & d2 = F1 . (Sub_the_right_argument_of S) implies F1 . S = H₁(d1,d2) ) & ( S is Sub_universal & d1 = F1 . (Sub_the_scope_of S) implies F1 . S = Quant (S,d1) ) ) ;
assume for S being Element of QC-Sub-WFF holds
( ( S is Sub_VERUM implies F2 . S = VERUM ) & ( S is Sub_atomic implies F2 . S = H₃(S) ) & ( S is Sub_negative implies F2 . S = H₂(F2 . (Sub_the_argument_of S)) ) & ( S is Sub_conjunctive implies F2 . S = H₁(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))) ) ) ; :: thesis: F1 = F2
then A2: for S being Element of QC-Sub-WFF
for d1, d2 being Element of QC-WFF holds
( ( S is Sub_VERUM implies F2 . S = VERUM ) & ( S is Sub_atomic implies F2 . S = H₃(S) ) & ( S is Sub_negative & d1 = F2 . (Sub_the_argument_of S) implies F2 . S = H₂(d1) ) & ( S is Sub_conjunctive & d1 = F2 . (Sub_the_left_argument_of S) & d2 = F2 . (Sub_the_right_argument_of S) implies F2 . S = H₁(d1,d2) ) & ( S is Sub_universal & d1 = F2 . (Sub_the_scope_of S) implies F2 . S = Quant (S,d1) ) ) ;
thus F1 = F2 from SUBSTUT1:sch 4(A1, A2); :: thesis: verum