let X be set ; :: thesis: for g2, f, g1 being Function st rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X holds
g1 = g2
let g2, f, g1 be Function; :: thesis: ( rng g2 = X & f * g2 = id (dom g1) & g1 * f = id X implies g1 = g2 )
assume that
A1: rng g2 = X and
A2: f * g2 = id (dom g1) and
A3: g1 * f = id X ; :: thesis: g1 = g2
( g1 * (f * g2) = (g1 * f) * g2 & g1 * (id (dom g1)) = g1 & (id X) * g2 = g2 ) by A1, RELAT_1:55, RELAT_1:77, RELAT_1:79;
hence g1 = g2 by A2, A3; :: thesis: verum