let y be set ; :: thesis: for C, D being non empty set

for f being PartFunc of C,D holds

( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D holds

( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

let f be PartFunc of C,D; :: thesis: ( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

thus ( y in rng f implies ex c being Element of C st

( c in dom f & y = f /. c ) ) :: thesis: ( ex c being Element of C st

( c in dom f & y = f /. c ) implies y in rng f )

A4: y = f /. c ; :: thesis: y in rng f

f . c in rng f by A3, FUNCT_1:def 3;

hence y in rng f by A3, A4, PARTFUN1:def 6; :: thesis: verum

for f being PartFunc of C,D holds

( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D holds

( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

let f be PartFunc of C,D; :: thesis: ( y in rng f iff ex c being Element of C st

( c in dom f & y = f /. c ) )

thus ( y in rng f implies ex c being Element of C st

( c in dom f & y = f /. c ) ) :: thesis: ( ex c being Element of C st

( c in dom f & y = f /. c ) implies y in rng f )

proof

given c being Element of C such that A3:
c in dom f
and
assume
y in rng f
; :: thesis: ex c being Element of C st

( c in dom f & y = f /. c )

then consider x being object such that

A1: x in dom f and

A2: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of C by A1;

take x ; :: thesis: ( x in dom f & y = f /. x )

thus ( x in dom f & y = f /. x ) by A1, A2, PARTFUN1:def 6; :: thesis: verum

end;( c in dom f & y = f /. c )

then consider x being object such that

A1: x in dom f and

A2: y = f . x by FUNCT_1:def 3;

reconsider x = x as Element of C by A1;

take x ; :: thesis: ( x in dom f & y = f /. x )

thus ( x in dom f & y = f /. x ) by A1, A2, PARTFUN1:def 6; :: thesis: verum

A4: y = f /. c ; :: thesis: y in rng f

f . c in rng f by A3, FUNCT_1:def 3;

hence y in rng f by A3, A4, PARTFUN1:def 6; :: thesis: verum