A3: 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] by A1;
consider D being Function such that
dom D = F₁() and
A4: for a being set st a in F₁() holds
for y being set holds
( y in D . a iff ( y in F₂(a) & P₁[a,y] ) ) from CARD_3:sch 4();
deffunc H₁( set ) -> set = D . $1;

let a be Element of F₁(); :: thesis:
for y being set holds
( y in D . a iff ( y in F₂(a) & P₁[a,y] ) ) by A4;
hence P₂[a,a, id H₁(a)] by A2; :: thesis:

end;

consider C being strict semi-functional para-functional set-id-inheriting category such that
A6: the carrier of C = F₁() and
A7: for a being object of C holds the_carrier_of a = H₁(a) and
A8: for a, b being Element of F₁()
for f being Function holds
( f in the Arrows of C . a,b iff ( f in Funcs H₁(a),H₁(b) & P₂[a,b,f] ) ) from YELLOW18:sch 17(A3, A5);
take C ; :: thesis:
thus the carrier of C = F₁() by A6; :: thesis:

let a be object of C; :: thesis:
the_carrier_of a = D . a by A7;
hence for x being set holds
( x in the_carrier_of a iff ( x in F₂(a) & P₁[a,x] ) ) by A4, A6; :: thesis:

end;

let a, b be Element of F₁(); :: thesis:
A9: D . a = C -carrier_of a by A6, A7;
D . b = C -carrier_of b by A6, A7;
hence 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) & P₂[a,b,f] ) ) by A8, A9; :: thesis: