let Y be set ; :: thesis: for f being Function st ( for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ) holds
Y c= rng f
let f be Function; :: thesis: ( ( for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ) implies Y c= rng f )
assume A1: for y being set st y in Y holds
ex x being set st
( x in dom f & y = f . x ) ; :: thesis: Y c= rng f
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng f )
assume y in Y ; :: thesis: y in rng f
then ex x being set st
( x in dom f & y = f . x ) by A1;
hence y in rng f by Def5; :: thesis: verum