for J being non empty set
for A, B being set
for f being Function of A,B
for g being Function of B,A st g * f = id A holds
(J => g) ** (J => f) = id (J --> A)