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 ));
deffunc H₂( Element of QC-WFF ) -> Element of QC-WFF = 'not' $1;
deffunc H₃( Element of QC-WFF , Element of QC-WFF ) -> Element of QC-WFF = $1 '&' $2;
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 )
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