let A be QC-alphabet ; :: thesis: for F1, F2 being Function of (QC-Sub-WFF A),(QC-WFF A) st ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( 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 A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( 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))) ) ) ) holds
F1 = F2
let F1, F2 be Function of (QC-Sub-WFF A),(QC-WFF A); :: thesis: ( ( for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( 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 A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( 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 A, Element of QC-WFF A) -> Element of QC-WFF A = $1 '&' $2;
deffunc H₂( Element of QC-WFF A) -> Element of QC-WFF A = 'not' $1;
deffunc H₃( Element of QC-Sub-WFF A) -> Element of QC-WFF A = (the_pred_symbol_of ($1 `1)) ! (CQC_Subst ((Sub_the_arguments_of $1),($1 `2)));
assume for S being Element of QC-Sub-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( 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 A st
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( 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 A
for d1, d2 being Element of QC-WFF A holds
( ( S is A -Sub_VERUM implies F1 . S = VERUM A ) & ( 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 A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( 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 A
for d1, d2 being Element of QC-WFF A holds
( ( S is A -Sub_VERUM implies F2 . S = VERUM A ) & ( 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