ex C being strict category st
( the carrier of C = F₁() & ( for a, b being Object of C
for f being set holds
( f in <^a,b^> iff ( f in F₂(a,b) & P₁[a,b,f] ) ) ) & ( for a, b, c being Object of C st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c holds g * f = F₃(a,b,c,f,g) ) )

A1: for a, b, c being Element of F₁()
for f, g being set st f in F₂(a,b) & P₁[a,b,f] & g in F₂(b,c) & P₁[b,c,g] holds
( F₃(a,b,c,f,g) in F₂(a,c) & P₁[a,c,F₃(a,b,c,f,g)] ) and
A2: for a, b, c, d being Element of F₁()
for f, g, h being set st f in F₂(a,b) & P₁[a,b,f] & g in F₂(b,c) & P₁[b,c,g] & h in F₂(c,d) & P₁[c,d,h] holds
F₃(a,c,d,F₃(a,b,c,f,g),h) = F₃(a,b,d,f,F₃(b,c,d,g,h)) and
A3: for a being Element of F₁() ex f being set st
( f in F₂(a,a) & P₁[a,a,f] & ( for b being Element of F₁()
for g being set st g in F₂(a,b) & P₁[a,b,g] holds
F₃(a,a,b,f,g) = g ) ) and
A4: for a being Element of F₁() ex f being set st
( f in F₂(a,a) & P₁[a,a,f] & ( for b being Element of F₁()
for g being set st g in F₂(b,a) & P₁[b,a,g] holds
F₃(b,a,a,g,f) = g ) )