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 )

proof

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;

given c being Element of C such that A3: c in dom f and
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