scheme :: QC_LANG3:sch 2
QCDefD{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> Element of F₂(), F₄() -> Element of QC-WFF F₁(), F₅( Element of QC-WFF F₁()) -> Element of F₂(), F₆( Element of F₂()) -> Element of F₂(), F₇( Element of F₂(), Element of F₂()) -> Element of F₂(), F₈( Element of QC-WFF F₁(), Element of F₂()) -> Element of F₂() } :

( ex d being Element of F₂() ex F being Function of (QC-WFF F₁()),F₂() st
( d = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) & ( for x1, x2 being Element of F₂() st ex F being Function of (QC-WFF F₁()),F₂() st
( x1 = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) & ex F being Function of (QC-WFF F₁()),F₂() st
( x2 = F . F₄() & ( for p being Element of QC-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( p = VERUM F₁() implies F . p = F₃() ) & ( p is atomic implies F . p = F₅(p) ) & ( p is negative & d1 = F . (the_argument_of p) implies F . p = F₆(d1) ) & ( p is conjunctive & d1 = F . (the_left_argument_of p) & d2 = F . (the_right_argument_of p) implies F . p = F₇(d1,d2) ) & ( p is universal & d1 = F . (the_scope_of p) implies F . p = F₈(p,d1) ) ) ) ) holds
x1 = x2 ) )