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