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

A3: dom ({} --> x) = {} ;
thus f = (dom f) --> x by A2, A3; :: thesis: verum

end;

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

consider z being 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 . z = y by A1, A4;
hence ex y1 being set st
( y1 in dom f & y = f . y1 ) by A4; :: 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 5;
hence f = (dom f) --> x by Th15; :: thesis: verum

end;

end;

end;

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