theorem :: FUNCOP_1:73

for a, b being object
for f being Function holds
( a .--> b c= f iff ( a in dom f & f . a = b ) )