scheme :: SUBSTUT1:sch 3
SubFuncEx{ F1() -> QC-alphabet , F2() -> non empty set , F3() -> Element of F2(), F4( Element of QC-Sub-WFF F1()) -> Element of F2(), F5( Element of F2()) -> Element of F2(), F6( Element of F2(), Element of F2()) -> Element of F2(), F7( set , Element of QC-Sub-WFF F1(), Element of F2()) -> Element of F2() } :
ex F being Function of (QC-Sub-WFF F1()),F2() st
for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )