let U be Grothendieck; :: thesis: for f being Function st dom f in U & rng f c= U holds
rng f in U
let f be Function; :: thesis: ( dom f in U & rng f c= U implies rng f in U )
assume A1: ( dom f in U & rng f c= U ) ; :: thesis: rng f in U
set A = dom f;
A2: ( U is epsilon-transitive & U is power-closed & U is FamUnion-closed ) ;
deffunc H₁( set ) -> set = {(f . $1)};
consider s being Function such that
A3: ( dom s = dom f & ( for X being set st X in dom f holds
s . X = H₁(X) ) ) from FUNCT_1:sch 5();
rng s c= U

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in U )
assume y in rng s ; :: thesis: y in U
then consider x being object such that
A4: ( x in dom s & s . x = y ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
f . x in rng f by A4, A3, FUNCT_1:def 3;
then bool (f . x) in U by A1, A2;
then A5: bool (bool (f . x)) c= U by A2;
H₁(x) c= bool (f . x) by ZFMISC_1:68;
then H₁(x) in bool (bool (f . x)) ;
then y in bool (bool (f . x)) by A4, A3;
hence y in U by A5; :: thesis: verum

end;

then A6: union (rng s) in U by A3, A1, A2;
A7: Union s c= rng f

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Union s or y in rng f )
assume y in Union s ; :: thesis: y in rng f
then consider x being object such that
A8: ( x in dom s & y in s . x ) by CARD_5:2;
reconsider x = x as set by TARSKI:1;
s . x = H₁(x) by A8, A3;
then y = f . x by A8, TARSKI:def 1;
hence y in rng f by A8, A3, FUNCT_1:def 3; :: thesis: verum

end;

rng f c= Union s

proof

let fx be object ; :: according to TARSKI:def 3 :: thesis: ( not fx in rng f or fx in Union s )
assume fx in rng f ; :: thesis: fx in Union s
then consider x being object such that
A9: ( x in dom f & f . x = fx ) by FUNCT_1:def 3;
reconsider x = x as set by A9;
( fx in H₁(x) & H₁(x) = s . x ) by A9, A3, TARSKI:def 1;
hence fx in Union s by A9, A3, CARD_5:2; :: thesis: verum

end;

then rng f = Union s by A7;
hence rng f in U by CARD_3:def 4, A6; :: thesis: verum