let f be Function; :: thesis: for x being object st ( for z being object st z in dom f holds
f . z = x ) holds
f = (dom f) --> x
let x be object ; :: thesis: ( ( for z being object st z in dom f holds
f . z = x ) implies f = (dom f) --> x )
assume A1: for z being object st z in dom f holds
f . z = x ; :: thesis: f = (dom f) --> x

now :: thesis: f = (dom f) --> x

per cases ( dom f = {} or dom f <> {} ) ;

suppose A2: dom f = {} ; :: thesis: f = (dom f) --> x

thus f = (dom f) --> x by A2; :: thesis: verum

end;

suppose A3: dom f <> {} ; :: thesis: f = (dom f) --> x

set z = the Element of dom f;

now :: thesis: for y being object holds
( ( y in {x} implies ex y1 being object st
( y1 in dom f & y = f . y1 ) ) & ( ex y1 being object st
( y1 in dom f & y = f . y1 ) implies y in {x} ) )

let y be object ; :: thesis: ( ( y in {x} implies ex y1 being object st
( y1 in dom f & y = f . y1 ) ) & ( ex y1 being object st
( y1 in dom f & y = f . y1 ) implies y in {x} ) )
thus ( y in {x} implies ex y1 being object st
( y1 in dom f & y = f . y1 ) ) :: thesis: ( ex y1 being object st
( y1 in dom f & y = f . y1 ) implies y in {x} )

proof

assume y in {x} ; :: thesis: ex y1 being object st
( y1 in dom f & y = f . y1 )
then y = x by TARSKI:def 1;
then f . the Element of dom f = y by A1, A3;
hence ex y1 being object st
( y1 in dom f & y = f . y1 ) by A3; :: thesis: verum

end;

assume ex y1 being object st
( y1 in dom f & y = f . y1 ) ; :: thesis: y in {x}
then y = x by A1;
hence y in {x} by TARSKI:def 1; :: thesis: verum

end;

then rng f = {x} by FUNCT_1:def 3;
hence f = (dom f) --> x by Th9; :: thesis: verum

end;

end;

end;

hence f = (dom f) --> x ; :: thesis: verum