let Y be set ; :: thesis: for f, g, h being Function st Y = rng f & dom g = Y & dom h = Y & g * f = h * f holds
g = h
let f, g, h be Function; :: thesis: ( Y = rng f & dom g = Y & dom h = Y & g * f = h * f implies g = h )
assume that
A1: Y = rng f and
A2: dom g = Y and
A3: dom h = Y and
A4: g * f = h * f ; :: thesis: g = h
for y being set st y in Y holds
g . y = h . y

proof

let y be set ; :: thesis: ( y in Y implies g . y = h . y )
assume y in Y ; :: thesis: g . y = h . y
then consider x being set such that
A5: x in dom f and
A6: y = f . x by A1, Def5;
( (g * f) . x = g . y & (h * f) . x = h . y ) by A5, A6, Th23;
hence g . y = h . y by A4; :: thesis: verum

end;

hence g = h by A2, A3, Th9; :: thesis: verum