let Y be set ; :: thesis: for f being Function st ( for y being object st y in Y holds
ex x being object st
( x in dom f & y = f . x ) ) holds
Y c= rng f
let f be Function; :: thesis: ( ( for y being object st y in Y holds
ex x being object st
( x in dom f & y = f . x ) ) implies Y c= rng f )
assume A1: for y being object st y in Y holds
ex x being object st
( x in dom f & y = f . x ) ; :: thesis: Y c= rng f
let y be object ; :: 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 object st
( x in dom f & y = f . x ) by A1;
hence y in rng f by Def3; :: thesis: verum