:: deftheorem defines R#8 FOMODEL4:def 59 :
for S being Language holds R#8 S = FuncRule (P#8 S);