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