theorem Th2: :: GLIB_010:2

for A being one-to-one Function
for C, D being Function st D * A = C | (dom A) holds
C * (A ") = D | (dom (A "))