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