let X be set ; :: thesis: for f, g1, g2 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds
g1 = g2
let f, g1, g2 be Function; :: thesis: ( rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X implies g1 = g2 )
A1: ( g1 * (f * g2) = (g1 * f) * g2 & g1 * (id (dom g1)) = g1 ) by RELAT_1:36, RELAT_1:51;
assume ( rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X ) ; :: thesis: g1 = g2
hence g1 = g2 by A1, RELAT_1:53; :: thesis: verum