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

now

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

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

dom ({} --> x) = {} ;
hence 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

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

proof

assume y in {x} ; :: thesis: ex y1 being set 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 set st
( y1 in dom f & y = f . y1 ) by A3; :: thesis: verum

end;

assume ex y1 being set 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 Th15; :: thesis: verum

end;

end;

end;

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