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

A4: now

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 by YELLOW16:1;
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 = (g * f) (#) h by YELLOW16:1
.= h * (g * f) by YELLOW16:1
.= (h * g) * f by RELAT_1:36
.= f (#) (h * g) by YELLOW16:1 ;
hence H₁(a,c,d,H₁(a,b,c,f,g),h) = H₁(a,b,d,f,H₁(b,c,d,g,h)) by YELLOW16:1; :: 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 = h * f by A15, YELLOW16:1
.= 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 = f * h by A19, YELLOW16:1
.= 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

proof

let a1, a2, a3 be object of C; :: according to ALTCAT_1:def 12 :: thesis:
assume that
A29: <^a1,a2^> <> {} and
A30: <^a2,a3^> <> {} and
<^a1,a3^> <> {} ; :: thesis:
let f be Morphism of a1,a2; :: thesis:
let g be Morphism of a2,a3; :: thesis:
let f9, g9 be Function; :: thesis:
assume that
A31: f = f9 and
A32: g = g9 ; :: thesis:
thus g * f = f9 (#) g9 by A23, A29, A30, A31, A32
.= g9 * f9 by YELLOW16:1 ; :: thesis:

end;

A33: now

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

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

end;

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

end;

A39: now

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 A33
.= dom (id F₃(a))
.= F₃(a) by RELAT_1:45
.= 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 A33
.= id (D . a) by A24
.= id (the_carrier_of a) by A39 ; :: 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 A39
.= F₃(a) by A24 ; :: thesis:

end;

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