deffunc H₁( Element of QC-WFF A, Element of QC-WFF A) -> Element of QC-WFF A = IFEQ ((bound_in $1),x,$1,(All ((bound_in $1),$2)));
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-WFF A) -> Element of QC-WFF A = (the_pred_symbol_of $1) ! (Subst ((the_arguments_of $1),((A a. 0) .--> x)));
consider F being Function of (QC-WFF A),(QC-WFF A) such that
A1: ( F . (VERUM A) = VERUM A & ( for p being Element of QC-WFF A holds
( ( p is atomic implies F . p = H₄(p) ) & ( p is negative implies F . p = H₃(F . (the_argument_of p)) ) & ( p is conjunctive implies F . p = H₂(F . (the_left_argument_of p),F . (the_right_argument_of p)) ) & ( p is universal implies F . p = H₁(p,F . (the_scope_of p)) ) ) ) ) from QC_LANG1:sch 3();
take F . p ; :: thesis: ex F being Function of (QC-WFF A),(QC-WFF A) st
( F . p = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) )
take F ; :: thesis: ( F . p = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) )
thus F . p = F . p ; :: thesis: for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) )
thus for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) by A1; :: thesis: verum