let U be Universe; :: thesis: for C being U -locally_small Category st the carrier of C is U -set holds
union { (Hom (a,b)) where a, b is Object of C : verum } is Element of U
let C be U -locally_small Category; :: thesis: ( the carrier of C is U -set implies union { (Hom (a,b)) where a, b is Object of C : verum } is Element of U )
assume A1: the carrier of C is U -set ; :: thesis: union { (Hom (a,b)) where a, b is Object of C : verum } is Element of U

A2: now :: thesis: for a being Object of C ex f being Function of the carrier of C,U st
for x being Object of C holds f . x = Hom (a,x)

let a be Object of C; :: thesis: ex f being Function of the carrier of C,U st
for x being Object of C holds f . x = Hom (a,x)
reconsider cC = the carrier of C as non empty set ;
reconsider c9C = the carrier' of C as non empty set ;
defpred S₁[ Object of C, Element of U] means Hom (a,$1) = $2;

A3: now :: thesis: for x being Element of the carrier of C ex y being Element of U st S₁[x,y]

let x be Element of the carrier of C; :: thesis: ex y being Element of U st S₁[x,y]
Hom (a,x) is U -set by Def36;
hence ex y being Element of U st S₁[x,y] ; :: thesis: verum

end;

ex f being Function of the carrier of C,U st
for x being Element of the carrier of C holds S₁[x,f . x] from FUNCT_2:sch 3(A3);
hence ex f being Function of the carrier of C,U st
for x being Object of C holds f . x = Hom (a,x) ; :: thesis: verum

end;

A4: now :: thesis: for a being Object of C holds union { (Hom (a,b)) where b is Object of C : verum } in U

let a be Object of C; :: thesis: union { (Hom (a,b)) where b is Object of C : verum } in U
consider f being Function of the carrier of C,U such that
A5: for x being Object of C holds f . x = Hom (a,x) by A2;

A6: now :: thesis: ( rng f c= { (Hom (a,b)) where b is Object of C : verum } & { (Hom (a,b)) where b is Object of C : verum } c= rng f )

now :: thesis: for t being object st t in rng f holds
t in { (Hom (a,b)) where b is Object of C : verum }

let t be object ; :: thesis: ( t in rng f implies t in { (Hom (a,b)) where b is Object of C : verum } )
assume t in rng f ; :: thesis: t in { (Hom (a,b)) where b is Object of C : verum }
then consider u being object such that
A7: u in the carrier of C and
A8: t = f . u by FUNCT_2:11;
reconsider u = u as Object of C by A7;
t = Hom (a,u) by A8, A5;
hence t in { (Hom (a,b)) where b is Object of C : verum } ; :: thesis: verum

end;

hence rng f c= { (Hom (a,b)) where b is Object of C : verum } ; :: thesis: { (Hom (a,b)) where b is Object of C : verum } c= rng f

now :: thesis: for t being object st t in { (Hom (a,b)) where b is Object of C : verum } holds
t in rng f

let t be object ; :: thesis: ( t in { (Hom (a,b)) where b is Object of C : verum } implies t in rng f )
assume t in { (Hom (a,b)) where b is Object of C : verum } ; :: thesis: t in rng f
then consider b being Object of C such that
A9: t = Hom (a,b) ;
t = f . b by A5, A9;
hence t in rng f by FUNCT_2:4; :: thesis: verum

end;

hence { (Hom (a,b)) where b is Object of C : verum } c= rng f ; :: thesis: verum

end;

then A10: rng f = { (Hom (a,b)) where b is Object of C : verum } ;

now :: thesis: for t being object st t in { (Hom (a,b)) where b is Object of C : verum } holds
t in U

let t be object ; :: thesis: ( t in { (Hom (a,b)) where b is Object of C : verum } implies t in U )
assume t in { (Hom (a,b)) where b is Object of C : verum } ; :: thesis: t in U
then consider b being Object of C such that
A11: t = Hom (a,b) ;
Hom (a,b) is U -set by Def36;
hence t in U by A11; :: thesis: verum

end;

then A12: rng f c= U by A6;
dom f = the carrier of C by PARTFUN1:def 2;
hence union { (Hom (a,b)) where b is Object of C : verum } in U by A1, A10, A12, CLASSES4:5; :: thesis: verum

end;

defpred S₁[ Object of C, Element of U] means union { (Hom ($1,b)) where b is Object of C : verum } = $2;

A13: now :: thesis: for x being Element of the carrier of C ex y being Element of U st S₁[x,y]

let x be Element of the carrier of C; :: thesis: ex y being Element of U st S₁[x,y]
reconsider y = union { (Hom (x,b)) where b is Object of C : verum } as Element of U by A4;
union { (Hom (x,b)) where b is Object of C : verum } = y ;
hence ex y being Element of U st S₁[x,y] ; :: thesis: verum

end;

consider f being Function of the carrier of C,U such that
A14: for x being Element of the carrier of C holds S₁[x,f . x] from FUNCT_2:sch 3(A13);
A15: for x being object st x in dom f holds
f . x in U

proof

let x be object ; :: thesis: ( x in dom f implies f . x in U )
assume x in dom f ; :: thesis: f . x in U
then reconsider x9 = x as Object of C by FUNCT_2:def 1;
f . x9 in U ;
hence f . x in U ; :: thesis: verum

end;

now :: thesis: for x being object st x in rng f holds
x in U

let x be object ; :: thesis: ( x in rng f implies x in U )
assume x in rng f ; :: thesis: x in U
then consider y being object such that
A16: y in the carrier of C and
A17: x = f . y by FUNCT_2:11;
dom f = the carrier of C by PARTFUN1:def 2;
hence x in U by A17, A16, A15; :: thesis: verum

end;

then A18: rng f c= U ;
A19: dom f in U by A1, PARTFUN1:def 2;

A20: now :: thesis: for x being object st x in rng f holds
ex y being Element of the carrier of C st union { (Hom (y,b)) where b is Object of C : verum } = x

let x be object ; :: thesis: ( x in rng f implies ex y being Element of the carrier of C st union { (Hom (y,b)) where b is Object of C : verum } = x )
assume x in rng f ; :: thesis: ex y being Element of the carrier of C st union { (Hom (y,b)) where b is Object of C : verum } = x
then consider y being object such that
A21: y in the carrier of C and
A22: x = f . y by FUNCT_2:11;
reconsider y = y as Element of the carrier of C by A21;
S₁[y,f . y] by A14;
hence ex y being Element of the carrier of C st union { (Hom (y,b)) where b is Object of C : verum } = x by A22; :: thesis: verum

end;

now :: thesis: ( union (rng f) c= union { (Hom (a,b)) where a, b is Object of C : verum } & union { (Hom (a,b)) where a, b is Object of C : verum } c= union (rng f) )

now :: thesis: for x being object st x in union (rng f) holds
x in union { (Hom (a,b)) where a, b is Object of C : verum }

let x be object ; :: thesis: ( x in union (rng f) implies x in union { (Hom (a,b)) where a, b is Object of C : verum } )
assume x in union (rng f) ; :: thesis: x in union { (Hom (a,b)) where a, b is Object of C : verum }
then consider y being set such that
A23: ( x in y & y in rng f ) by TARSKI:def 4;
consider z being Element of the carrier of C such that
A24: y = union { (Hom (z,b)) where b is Object of C : verum } by A23, A20;
reconsider z = z as Object of C ;
consider t being set such that
A25: ( x in t & t in { (Hom (z,b)) where b is Object of C : verum } ) by A23, A24, TARSKI:def 4;
consider b0 being Object of C such that
A26: t = Hom (z,b0) by A25;
( x in Hom (z,b0) & Hom (z,b0) in { (Hom (a,b)) where a, b is Object of C : verum } ) by A25, A26;
hence x in union { (Hom (a,b)) where a, b is Object of C : verum } by TARSKI:def 4; :: thesis: verum

end;

hence union (rng f) c= union { (Hom (a,b)) where a, b is Object of C : verum } ; :: thesis: union { (Hom (a,b)) where a, b is Object of C : verum } c= union (rng f)

now :: thesis: for x being object st x in union { (Hom (a,b)) where a, b is Object of C : verum } holds
x in union (rng f)

let x be object ; :: thesis: ( x in union { (Hom (a,b)) where a, b is Object of C : verum } implies x in union (rng f) )
assume x in union { (Hom (a,b)) where a, b is Object of C : verum } ; :: thesis: x in union (rng f)
then consider y being set such that
A27: ( x in y & y in { (Hom (a,b)) where a, b is Object of C : verum } ) by TARSKI:def 4;
consider a9, b9 being Object of C such that
A28: y = Hom (a9,b9) by A27;
reconsider a9 = a9 as Element of the carrier of C ;
y in { (Hom (a9,b)) where b is Object of C : verum } by A28;
then A29: x in union { (Hom (a9,b)) where b is Object of C : verum } by A27, TARSKI:def 4;
A30: union { (Hom (a9,b)) where b is Object of C : verum } = f . a9 by A14;
f . a9 in rng f by FUNCT_2:4;
hence x in union (rng f) by A30, A29, TARSKI:def 4; :: thesis: verum

end;

hence union { (Hom (a,b)) where a, b is Object of C : verum } c= union (rng f) ; :: thesis: verum

end;

then union (rng f) = union { (Hom (a,b)) where a, b is Object of C : verum } ;
hence union { (Hom (a,b)) where a, b is Object of C : verum } is Element of U by A19, A18, CLASSES4:5; :: thesis: verum