thus ex C9 being strict concrete category st
( the carrier of C9 = the carrier of C & ( for a being Object of C9
for x being set holds
( x in the_carrier_of a iff ( x in H₁(a) & S₁[a,x] ) ) ) & ( for a, b being Element of C
for f being Function holds
( f in the Arrows of C9 . (a,b) iff ( f in Funcs ((C9 -carrier_of a),(C9 -carrier_of b)) & S₂[a,b,f] ) ) ) ) from YELLOW18:sch 18(A1, A13); :: thesis: verum