theorem Th4: :: GROUP_21:6

for I, J being non empty set
for a being Function of I,J
for x, y being Function st dom x = I & dom y = J & a is bijective holds
( x = y * a iff y = x * (a ") )