for X, X1 being set
for F being Function st X c= F " X1 holds
F .: X c= X1