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

proof

deffunc H₁( set ) -> set = {} ;
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng f )
assume that
A3: y in Y and
A4: not y in rng f ; :: thesis: contradiction
defpred S₁[ set , set ] means ( ( $1 = y implies $2 = 1 ) & ( $1 <> y implies $2 = {} ) );
A5: for x being set st x in Y holds
ex y1 being set st S₁[x,y1]

proof

let x be set ; :: thesis: ( x in Y implies ex y1 being set st S₁[x,y1] )
assume x in Y ; :: thesis: ex y1 being set st S₁[x,y1]
( x = y implies ex y1 being set st S₁[x,y1] ) ;
hence ex y1 being set st S₁[x,y1] ; :: thesis: verum

end;

A6: for x, y1, y2 being set st x in Y & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
consider h being Function such that
A7: dom h = Y and
A8: for x being set st x in Y holds
S₁[x,h . x] from FUNCT_1:sch 2(A6, A5);
A9: dom (h * f) = dom f by A1, A7, RELAT_1:46;
consider g being Function such that
A10: dom g = Y and
A11: for x being set st x in Y holds
g . x = H₁(x) from FUNCT_1:sch 3();
A12: dom (g * f) = dom f by A1, A10, RELAT_1:46;
for x being set st x in dom f holds
(g * f) . x = (h * f) . x

proof

let x be set ; :: thesis: ( x in dom f implies (g * f) . x = (h * f) . x )
assume A13: x in dom f ; :: thesis: (g * f) . x = (h * f) . x
then f . x in rng f by Def5;
then A14: ( g . (f . x) = {} & h . (f . x) = {} ) by A1, A4, A11, A8;
(g * f) . x = g . (f . x) by A12, A13, Th22;
hence (g * f) . x = (h * f) . x by A9, A13, A14, Th22; :: thesis: verum

end;

then A15: g = h by A2, A10, A7, A12, A9, Th9;
g . y = {} by A3, A11;
hence contradiction by A3, A8, A15; :: thesis: verum

end;

hence Y = rng f by A1, XBOOLE_0:def 10; :: thesis: verum