theorem Th3: :: FUNCTOR0:3

for A being set
for f being Function holds f .: (id A) = (~ f) .: (id A)