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