thus ex C' being strict concrete category st
( the carrier of C' = the carrier of C & ( for a being object of C'
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 C' . a,b iff ( f in Funcs (C' -carrier_of a),(C' -carrier_of b) & S₂[a,b,f] ) ) ) ) from YELLOW18:sch 18(A1, A9); :: thesis: verum