scheme :: SUBSTUT1:sch 3
SubFuncEx{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> Element of F₂(), F₄( Element of QC-Sub-WFF F₁()) -> Element of F₂(), F₅( Element of F₂()) -> Element of F₂(), F₆( Element of F₂(), Element of F₂()) -> Element of F₂(), F₇( set , Element of QC-Sub-WFF F₁(), Element of F₂()) -> Element of F₂() } :

ex F being Function of (QC-Sub-WFF F₁()),F₂() st
for S being Element of QC-Sub-WFF F₁()
for d1, d2 being Element of F₂() holds
( ( S is F₁() -Sub_VERUM implies F . S = F₃() ) & ( S is Sub_atomic implies F . S = F₄(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F₅(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F₆(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F₇(F₁(),S,d1) ) )