ex C being strict concrete category st
( the carrier of C = F₁() & ( for a being Object of C holds the_carrier_of a = F₂(a) ) & ( for a, b being Element of F₁()
for f being Function holds
( f in the Arrows of C . (a,b) iff ( f in Funcs (F₂(a),F₂(b)) & P₁[a,b,f] ) ) ) )

A1: for a, b, c being Element of F₁()
for f, g being Function st P₁[a,b,f] & P₁[b,c,g] holds
P₁[a,c,g * f] and
A2: for a being Element of F₁() holds P₁[a,a, id F₂(a)]