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₁( object ) -> set = {} ;
let y be object ; :: 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₁[ object , object ] means ( ( $1 = y implies $2 = {{}} ) & ( $1 <> y implies $2 = {} ) );
A5: for x being object st x in Y holds
ex y1 being object st S₁[x,y1]

proof

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

end;

A6: for x, y1, y2 being object 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 object 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:27;
consider g being Function such that
A10: dom g = Y and
A11: for x being object 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:27;
for x being object st x in dom f holds
(g * f) . x = (h * f) . x

proof

let x be object ; :: 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 Def3;
then A14: ( g . (f . x) = {} & h . (f . x) = {} ) by A1, A4, A11, A8;
(g * f) . x = g . (f . x) by A12, A13, Th12;
hence (g * f) . x = (h * f) . x by A9, A13, A14, Th12; :: thesis: verum

end;

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

end;

hence Y = rng f by A1; :: thesis: verum