theorem Th13: :: HILBERT3:14

for a, b, c, d being set
for f being Function st a <> b & c in dom f & d in dom f holds
f * ((a,b) --> (c,d)) = (a,b) --> ((f . c),(f . d))