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