deffunc H₁( set , set , set , set , set ) -> set = $4 (#) $5;

A4: now :: thesis:

let a, b be Element of F₁(); :: thesis:
let f be set ; :: thesis:
assume A5: f in F₂(a,b) ; :: thesis:
F₂(a,b) c= Funcs (F₃(a),F₃(b)) by A2;
hence f is Function by A5; :: thesis:

end;

A6: for a, b, c being Element of F₁()
for f, g being set st f in F₂(a,b) & g in F₂(b,c) holds
H₁(a,b,c,f,g) in F₂(a,c)

proof

let a, b, c be Element of F₁(); :: thesis:
let f, g be set ; :: thesis:
assume that
A7: f in F₂(a,b) and
A8: g in F₂(b,c) ; :: thesis:
reconsider f = f, g = g as Function by A4, A7, A8;
g * f = f (#) g ;
hence H₁(a,b,c,f,g) in F₂(a,c) by A1, A7, A8; :: thesis:

end;

A9: for a, b, c, d being Element of F₁()
for f, g, h being set st f in F₂(a,b) & g in F₂(b,c) & h in F₂(c,d) holds
H₁(a,c,d,H₁(a,b,c,f,g),h) = H₁(a,b,d,f,H₁(b,c,d,g,h))

proof

let a, b, c, d be Element of F₁(); :: thesis:
let f, g, h be set ; :: thesis:
assume that
A10: f in F₂(a,b) and
A11: g in F₂(b,c) and
A12: h in F₂(c,d) ; :: thesis:
reconsider f = f, g = g, h = h as Function by A4, A10, A11, A12;
(f (#) g) (#) h = f (#) (h * g) by RELAT_1:36;
hence H₁(a,c,d,H₁(a,b,c,f,g),h) = H₁(a,b,d,f,H₁(b,c,d,g,h)) ; :: thesis:

end;

A13: for a being Element of F₁() ex f being set st
( f in F₂(a,a) & ( for b being Element of F₁()
for g being set st g in F₂(a,b) holds
H₁(a,a,b,f,g) = g ) )

proof

let a be Element of F₁(); :: thesis:
take f = id F₃(a); :: thesis:
thus f in F₂(a,a) by A3; :: thesis:
let b be Element of F₁(); :: thesis:
let g be set ; :: thesis:
assume A14: g in F₂(a,b) ; :: thesis:
F₂(a,b) c= Funcs (F₃(a),F₃(b)) by A2;
then consider h being Function such that
A15: g = h and
A16: dom h = F₃(a) and
rng h c= F₃(b) by A14, FUNCT_2:def 2;
thus f (#) g = g by A15, A16, RELAT_1:52; :: thesis:

end;

A17: for a being Element of F₁() ex f being set st
( f in F₂(a,a) & ( for b being Element of F₁()
for g being set st g in F₂(b,a) holds
H₁(b,a,a,g,f) = g ) )

proof

let a be Element of F₁(); :: thesis:
take f = id F₃(a); :: thesis:
thus f in F₂(a,a) by A3; :: thesis:
let b be Element of F₁(); :: thesis:
let g be set ; :: thesis:
assume A18: g in F₂(b,a) ; :: thesis:
F₂(b,a) c= Funcs (F₃(b),F₃(a)) by A2;
then consider h being Function such that
A19: g = h and
dom h = F₃(b) and
A20: rng h c= F₃(a) by A18, FUNCT_2:def 2;
thus g (#) f = g by A19, A20, RELAT_1:53; :: thesis:

end;

consider C being strict category such that
A21: the carrier of C = F₁() and
A22: for a, b being Object of C holds <^a,b^> = F₂(a,b) and
A23: 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 = H₁(a,b,c,f,g) from YELLOW18:sch 4(A6, A9, A13, A17);
consider D being ManySortedSet of C such that
A24: for x being Element of C holds D . x = F₃(x) from PBOOLE:sch 5();
A25: C is para-functional

proof

take D ; :: according to YELLOW18:def 7 :: thesis:
let a1, a2 be Object of C; :: thesis:
A26: <^a1,a2^> = F₂(a1,a2) by A22;
A27: F₃(a1) = D . a1 by A24;
F₃(a2) = D . a2 by A24;
hence <^a1,a2^> c= Funcs ((D . a1),(D . a2)) by A2, A21, A26, A27; :: thesis:

end;

A28: C is semi-functional by A23;

A29: now :: thesis:

let a be Object of C; :: thesis:
id F₃(a) in F₂(a,a) by A3, A21;
then reconsider e = id F₃(a) as Morphism of a,a by A22;

now :: thesis:

let b be Object of C; :: thesis:
assume A30: <^a,b^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
A31: <^a,b^> = F₂(a,b) by A22;
A32: F₂(a,b) c= Funcs (F₃(a),F₃(b)) by A2, A21;
f in <^a,b^> by A30;
then consider h being Function such that
A33: f = h and
A34: dom h = F₃(a) and
rng h c= F₃(b) by A31, A32, FUNCT_2:def 2;
thus f * e = h * (id F₃(a)) by A28, A30, A33
.= f by A33, A34, RELAT_1:52 ; :: thesis:

end;

hence idm a = id F₃(a) by ALTCAT_1:def 17; :: thesis:

end;

A35: now :: thesis:

let i be set ; :: thesis:
assume i in the carrier of C ; :: thesis:
then reconsider a = i as Object of C ;
thus C -carrier_of i = proj1 (idm a) by Def8
.= proj1 (id F₃(a)) by A29
.= F₃(a)
.= D . i by A24 ; :: thesis:

end;

C is set-id-inheriting

proof

let a be Object of C; :: according to YELLOW18:def 10 :: thesis:
thus idm a = id F₃(a) by A29
.= id (D . a) by A24
.= id (the_carrier_of a) by A35 ; :: thesis:

end;

then reconsider C = C as strict semi-functional para-functional set-id-inheriting category by A25, A28;
take C ; :: thesis:
thus the carrier of C = F₁() by A21; :: thesis:

hereby :: thesis:

let a be Object of C; :: thesis:
thus the_carrier_of a = D . a by A35
.= F₃(a) by A24 ; :: thesis:

end;

thus for a, b being Object of C holds <^a,b^> = F₂(a,b) by A22; :: thesis: