let Y1, Y2 be set ; :: thesis: for f being Function st f " Y1 c= f " Y2 & Y1 c= rng f holds
Y1 c= Y2
let f be Function; :: thesis: ( f " Y1 c= f " Y2 & Y1 c= rng f implies Y1 c= Y2 )
assume that
A1: f " Y1 c= f " Y2 and
A2: Y1 c= rng f ; :: thesis: Y1 c= Y2
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Y1 or y in Y2 )
assume A3: y in Y1 ; :: thesis: y in Y2
then consider x being set such that
A4: x in dom f and
A5: y = f . x by A2, Def5;
x in f " Y1 by A3, A4, A5, Def13;
hence y in Y2 by A1, A5, Def13; :: thesis: verum