deffunc H₁( Element of QC-WFF A) -> Subset of (bound_QC-variables A) = Bound_Vars (the_arguments_of $1);
set V = bound_QC-variables A;
deffunc H₂( Subset of (bound_QC-variables A)) -> Subset of (bound_QC-variables A) = $1;
deffunc H₃( Subset of (bound_QC-variables A), Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $1 \/ $2;
deffunc H₄( Element of QC-WFF A, Subset of (bound_QC-variables A)) -> Element of bool (bound_QC-variables A) = $2 \/ {(bound_in $1)};
thus ( ex d being Subset of (bound_QC-variables A) ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( d = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H₁(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₂(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₃(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₄(p,d1) ) ) ) ) & ( for x1, x2 being Subset of (bound_QC-variables A) st ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( x1 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H₁(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₂(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₃(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₄(p,d1) ) ) ) ) & ex F being Function of (QC-WFF A),(bool (bound_QC-variables A)) st
( x2 = F . p & ( for p being Element of QC-WFF A
for d1, d2 being Subset of (bound_QC-variables A) holds
( ( p = VERUM A implies F . p = {} (bound_QC-variables A) ) & ( p is atomic implies F . p = H₁(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = H₂(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = H₃(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = H₄(p,d1) ) ) ) ) holds
x1 = x2 ) ) from QC_LANG3:sch 2(); :: thesis: verum