scheme :: MODAL_1:sch 2
MPFuncEx{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃( Element of MP-variables ) -> Element of F₁(), F₄( Element of F₁()) -> Element of F₁(), F₅( Element of F₁()) -> Element of F₁(), F₆( Element of F₁(), Element of F₁()) -> Element of F₁() } :

ex f being Function of MP-WFF,F₁() st
( f . VERUM = F₂() & ( for p being MP-variable holds f . (@ p) = F₃(p) ) & ( for A being Element of MP-WFF holds f . ('not' A) = F₄((f . A)) ) & ( for A being Element of MP-WFF holds f . ((#) A) = F₅((f . A)) ) & ( for A, B being Element of MP-WFF holds f . (A '&' B) = F₆((f . A),(f . B)) ) )