scheme :: QC_LANG1:sch 3
QCFuncEx{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> Element of 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 F being Function of (QC-WFF F₁()),F₂() st
( F . (VERUM F₁()) = F₃() & ( for p being Element of QC-WFF F₁() holds
( ( p is atomic implies F . p = F₄(p) ) & ( p is negative implies F . p = F₅((F . (the_argument_of p))) ) & ( p is conjunctive implies F . p = F₆((F . (the_left_argument_of p)),(F . (the_right_argument_of p))) ) & ( p is universal implies F . p = F₇(p,(F . (the_scope_of p))) ) ) ) )