:: deftheorem Def3 defines | TMAP_1:def 3 :
for S, T being 1-sorted
for f being Function of S,T
for R being 1-sorted st the carrier of R c= the carrier of S holds
f | R = f | the carrier of R;