theorem :: GLIBPRE1:9

for f being Function
for g being one-to-one Function holds (f +* g) * (g ") = id (rng g)