:: deftheorem defines ! ZF_LANG1:def 1 :
for D, D1, D2 being non empty set
for f being Function of D,D1 st D1 c= D2 holds
D2 ! f = f;