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