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

F₃() = F₄()

provided

A1: 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) ) ) and
A2: 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) ) )