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 H1( 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 = H1(X) ) ) from 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 ;
then bool (f . x) in U by A1, A2;
then A5: bool (bool (f . x)) c= U by A2;
H1(x) c= bool (f . x) by ZFMISC_1:68;
then H1(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 = H1(x) by A8, A3;
then y = f . x by ;
hence y in rng f by ; :: 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 H1(x) & H1(x) = s . x ) by ;
hence fx in Union s by ; :: thesis: verum
end;
then rng f = Union s by A7;
hence rng f in U by ; :: thesis: verum