:: deftheorem defines R#3a FOMODEL4:def 51 :
for S being Language holds R#3a S = FuncRule (P#3a S);