:: deftheorem Def47 defines FuncRule FOMODEL4:def 47 :
for S being Language
for R being Relation of (bool (S -sequents)),(S -sequents)
for b₃ being Rule of S holds
( b₃ = FuncRule R iff for inseqs being set st inseqs in bool (S -sequents) holds
b₃ . inseqs = { x where x is Element of S -sequents : [inseqs,x] in R } );