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

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) --> xend;

hence
f = (dom f) --> x
; :: thesis: verumper cases
( dom f = {} or dom f <> {} )
;

end;

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

set z = the Element of dom f;

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

end;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} ) )

then
rng f = {x}
by FUNCT_1:def 3;( ( 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} )

( 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;( 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
ex y1 being object st
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;( 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

( 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

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