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