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