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 & dom h = Y ) and
A3: g * f = h * f ; :: thesis: g = h
for y being object st y in Y holds
g . y = h . y

proof

let y be object ; :: thesis: ( y in Y implies g . y = h . y )
assume y in Y ; :: thesis: g . y = h . y
then consider x being object such that
A4: ( x in dom f & y = f . x ) by A1, Def3;
(g * f) . x = g . y by A4, Th13;
hence g . y = h . y by A3, A4, Th13; :: thesis: verum

end;

hence g = h by A2, Th2; :: thesis: verum