let C be Category; :: thesis: for O being non empty Subset of the carrier of C holds union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C
let O be non empty Subset of the carrier of C; :: thesis: union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C
set H = { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ;
set M = union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ;

now

now

consider a being Element of O;
reconsider a = a as Object of C ;
( id a in Hom a,a & Hom a,a in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ) by CAT_1:55;
then id a in union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;
hence ex f being set st f in union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: verum

end;

hence union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } is non empty set ; :: thesis: union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } c= the carrier' of C
thus union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } c= the carrier' of C :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } or x in the carrier' of C )
assume x in union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: x in the carrier' of C
then consider X being set such that
A1: x in X and
A2: X in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;
consider a, b being Object of C such that
A3: X = Hom a,b and
( a in O & b in O ) by A2;
thus x in the carrier' of C by A1, A3; :: thesis: verum

end;

end;

hence union { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C ; :: thesis: verum