deffunc H₁( object ) -> set = F₂(($1 `1),($1 `2));
defpred S₁[ object , object ] means P₁[$1 `1 ,$1 `2 ,$2];
consider P being Function such that
dom P = [:F₁(),F₁():] and
A5: for i being object st i in [:F₁(),F₁():] holds
for x being object holds
( x in P . i iff ( x in H₁(i) & S₁[i,x] ) ) from CARD_3:sch 2();
deffunc H₂( set , set ) -> set = P . ($1,$2);

let a, b be Element of F₁(); :: thesis:
let x be set ; :: thesis:
A7: [a,b] `1 = a ;
A8: [a,b] `2 = b ;
[a,b] in [:F₁(),F₁():] by ZFMISC_1:def 2;
hence ( x in P . (a,b) iff ( x in F₂(a,b) & P₁[a,b,x] ) ) by A5, A7, A8; :: thesis:

end;

end;

let a, b, c, d be Element of F₁(); :: thesis:
let f, g, h be set ; :: thesis:
assume that
A18: f in H₂(a,b) and
A19: g in H₂(b,c) and
A20: h in H₂(c,d) ; :: thesis:
A21: f in F₂(a,b) by A6, A18;
A22: P₁[a,b,f] by A6, A18;
A23: g in F₂(b,c) by A6, A19;
A24: P₁[b,c,g] by A6, A19;
A25: h in F₂(c,d) by A6, A20;
P₁[c,d,h] by A6, A20;
hence F₃(a,c,d,F₃(a,b,c,f,g),h) = F₃(a,b,d,f,F₃(b,c,d,g,h)) by A2, A21, A22, A23, A24, A25; :: thesis:

end;

let a be Element of F₁(); :: thesis:
consider f being set such that
A27: f in F₂(a,a) and
A28: P₁[a,a,f] and
A29: 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 by A3;
take f = f; :: thesis:
thus f in H₂(a,a) by A6, A27, A28; :: thesis:
let b be Element of F₁(); :: thesis:
let g be set ; :: thesis:
assume A30: g in H₂(a,b) ; :: thesis:
then A31: g in F₂(a,b) by A6;
P₁[a,b,g] by A6, A30;
hence F₃(a,a,b,f,g) = g by A29, A31; :: thesis:

end;

let a be Element of F₁(); :: thesis:
consider f being set such that
A33: f in F₂(a,a) and
A34: P₁[a,a,f] and
A35: 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 by A4;
take f = f; :: thesis:
thus f in H₂(a,a) by A6, A33, A34; :: thesis:
let b be Element of F₁(); :: thesis:
let g be set ; :: thesis:
assume A36: g in H₂(b,a) ; :: thesis:
then A37: g in F₂(b,a) by A6;
P₁[b,a,g] by A6, A36;
hence F₃(b,a,a,g,f) = g by A35, A37; :: thesis:

end;

consider C being strict category such that
A38: the carrier of C = F₁() and
A39: for a, b being Object of C holds <^a,b^> = H₂(a,b) and
A40: 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) from YELLOW18:sch 4(A9, A17, A26, A32);
take C ; :: thesis:
thus the carrier of C = F₁() by A38; :: thesis:

let a, b be Object of C; :: thesis:
let f be set ; :: thesis:
<^a,b^> = P . (a,b) by A39;
hence ( f in <^a,b^> iff ( f in F₂(a,b) & P₁[a,b,f] ) ) by A6, A38; :: thesis:

end;

thus 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) by A40; :: thesis: