let Y be set ; :: thesis: for f being Function st Y c= rng f holds
f .: (f " Y) = Y
let f be Function; :: thesis: ( Y c= rng f implies f .: (f " Y) = Y )
assume A1: Y c= rng f ; :: thesis: f .: (f " Y) = Y
thus f .: (f " Y) c= Y by Th74; :: according to XBOOLE_0:def 10 :: thesis: Y c= f .: (f " Y)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in f .: (f " Y) )
assume A2: y in Y ; :: thesis: y in f .: (f " Y)
then consider x being object such that
A3: ( x in dom f & y = f . x ) by A1, Def3;
x in f " Y by A2, A3, Def7;
hence y in f .: (f " Y) by A3, Def6; :: thesis: verum