:: deftheorem Def12 defines Concretized YELLOW18:def 12 :
for C being category
for b₂ being strict concrete category holds
( b₂ = Concretized C iff ( the carrier of b₂ = the carrier of C & ( for a being Object of b₂
for x being set holds
( x in the_carrier_of a iff ( x in Union (disjoin the Arrows of C) & a = x `22 ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of b₂ . (a,b) iff ( f in Funcs ((b₂ -carrier_of a),(b₂ -carrier_of b)) & ex fa, fb being Object of C ex g being Morphism of fa,fb st
( fa = a & fb = b & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(g * h),[o,fb]] ) ) ) ) ) ) );