scheme :: CQC_LANG:sch 3
CQCFuncUniq{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> Function of (CQC-WFF F₁()),F₂(), F₄() -> Function of (CQC-WFF F₁()),F₂(), F₅() -> Element of F₂(), F₆( set , set , 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: ( F₃() . (VERUM F₁()) = F₅() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds
( F₃() . (P ! l) = F₆(k,P,l) & F₃() . ('not' r) = F₇((F₃() . r)) & F₃() . (r '&' s) = F₈((F₃() . r),(F₃() . s)) & F₃() . (All (x,r)) = F₉(x,(F₃() . r)) ) ) ) and
A2: ( F₄() . (VERUM F₁()) = F₅() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds
( F₄() . (P ! l) = F₆(k,P,l) & F₄() . ('not' r) = F₇((F₄() . r)) & F₄() . (r '&' s) = F₈((F₄() . r),(F₄() . s)) & F₄() . (All (x,r)) = F₉(x,(F₄() . r)) ) ) )