deffunc H₁( set ) -> set = $1;
A13: the carrier of (Concretized A) = the carrier of A by Def12;
A14: for a being Object of A holds H₁(a) is Object of (Concretized A) by Def12;
reconsider AA = the Arrows of (Concretized A) as ManySortedSet of [: the carrier of A, the carrier of A:] by A13;
defpred S₁[ object , object , object ] means ex a, b being Object of A ex f being Morphism of a,b ex G being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) st
( $1 = [a,b] & $2 = f & $3 = G & ( for c being Object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
G . [g,[c,a]] = [(f * g),[c,b]] ) );
A15: for i, x being object st i in [: the carrier of A, the carrier of A:] & x in the Arrows of A . i holds
ex y being object st
( y in AA . i & S₁[i,x,y] )

let i, x be object ; :: thesis:
assume i in [: the carrier of A, the carrier of A:] ; :: thesis:
then consider a, b being object such that
A16: a in the carrier of A and
A17: b in the carrier of A and
A18: i = [a,b] by ZFMISC_1:def 2;
reconsider a = a, b = b as Object of A by A16, A17;
assume A19: x in the Arrows of A . i ; :: thesis:
then reconsider f = x as Morphism of a,b by A18;
consider G being Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) such that
A20: G in AA . (a,b) and
A21: for c being Object of A
for g being Morphism of c,a st <^c,a^> <> {} holds
G . [g,[c,a]] = [(f * g),[c,b]] by A18, A19, Th44;
take G ; :: thesis:
thus ( G in AA . i & S₁[i,x,G] ) by A18, A20, A21; :: thesis:

end;

consider F being ManySortedFunction of the Arrows of A,AA such that
A22: for i, x being object st i in [: the carrier of A, the carrier of A:] & x in the Arrows of A . i holds
( (F . i) . x in AA . i & S₁[i,x,(F . i) . x] ) from YELLOW18:sch 23(A15);
deffunc H₂( set , set , set ) -> set = (F . [$1,$2]) . $3;
A23: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds H₂(a,b,f) in the Arrows of (Concretized A) . (H₁(a),H₁(b))

proof

let a, b be Object of A; :: thesis:
assume A24: <^a,b^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
[a,b] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
hence H₂(a,b,f) in the Arrows of (Concretized A) . (H₁(a),H₁(b)) by A22, A24; :: thesis:

end;

A25: for a, b, c being Object of A st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of a,b
for g being Morphism of b,c
for a9, b9, c9 being Object of (Concretized A) st a9 = H₁(a) & b9 = H₁(b) & c9 = H₁(c) holds
for f9 being Morphism of a9,b9
for g9 being Morphism of b9,c9 st f9 = H₂(a,b,f) & g9 = H₂(b,c,g) holds
H₂(a,c,g * f) = g9 * f9

proof

let a, b, c be Object of A; :: thesis:
assume that
A26: <^a,b^> <> {} and
A27: <^b,c^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
let g be Morphism of b,c; :: thesis:
let a9, b9, c9 be Object of (Concretized A); :: thesis:
assume that
A28: a9 = a and
A29: b9 = b and
A30: c9 = c ; :: thesis:
let f9 be Morphism of a9,b9; :: thesis:
let g9 be Morphism of b9,c9; :: thesis:
assume that
A31: f9 = (F . [a,b]) . f and
A32: g9 = (F . [b,c]) . g ; :: thesis:
A33: [a,b] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider a1, b1 being Object of A, f1 being Morphism of a1,b1, G1 being Function of ((Concretized A) -carrier_of a1),((Concretized A) -carrier_of b1) such that
A34: [a,b] = [a1,b1] and
A35: f = f1 and
A36: (F . [a,b]) . f = G1 and
A37: for c being Object of A
for g being Morphism of c,a1 st <^c,a1^> <> {} holds
G1 . [g,[c,a1]] = [(f1 * g),[c,b1]] by A22, A26;
A38: [b,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider b2, c2 being Object of A, g2 being Morphism of b2,c2, G2 being Function of ((Concretized A) -carrier_of b2),((Concretized A) -carrier_of c2) such that
A39: [b,c] = [b2,c2] and
A40: g = g2 and
A41: (F . [b,c]) . g = G2 and
A42: for c being Object of A
for g being Morphism of c,b2 st <^c,b2^> <> {} holds
G2 . [g,[c,b2]] = [(g2 * g),[c,c2]] by A22, A27;
A43: <^a,c^> <> {} by A26, A27, ALTCAT_1:def 2;
[a,c] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider a3, c3 being Object of A, h3 being Morphism of a3,c3, G3 being Function of ((Concretized A) -carrier_of a3),((Concretized A) -carrier_of c3) such that
A44: [a,c] = [a3,c3] and
A45: g * f = h3 and
A46: (F . [a,c]) . (g * f) = G3 and
A47: for c being Object of A
for g being Morphism of c,a3 st <^c,a3^> <> {} holds
G3 . [g,[c,a3]] = [(h3 * g),[c,c3]] by A22, A43;
A48: (F . [a,b]) . f in <^a9,b9^> by A22, A26, A28, A29, A33;
A49: (F . [b,c]) . g in <^b9,c9^> by A22, A27, A29, A30, A38;
A50: a = a1 by A34, XTUPLE_0:1;
A51: b = b1 by A34, XTUPLE_0:1;
A52: b = b2 by A39, XTUPLE_0:1;
A53: c = c2 by A39, XTUPLE_0:1;
A54: a = a3 by A44, XTUPLE_0:1;
A55: c = c3 by A44, XTUPLE_0:1;
reconsider G1 = G1 as Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of b) by A34, A50, XTUPLE_0:1;
reconsider G2 = G2 as Function of ((Concretized A) -carrier_of b),((Concretized A) -carrier_of c) by A39, A52, XTUPLE_0:1;
reconsider G3 = G3 as Function of ((Concretized A) -carrier_of a),((Concretized A) -carrier_of c) by A44, A54, XTUPLE_0:1;

now :: thesis:

let x be Element of (Concretized A) -carrier_of a; :: thesis:
consider bb being Object of A, ff being Morphism of bb,a such that
A56: <^bb,a^> <> {} and
A57: x = [ff,[bb,a]] by Th43;
A58: <^bb,b^> <> {} by A26, A56, ALTCAT_1:def 2;
thus G3 . x = [((g * f) * ff),[bb,c]] by A45, A47, A54, A55, A56, A57
.= [(g * (f * ff)),[bb,c]] by A26, A27, A56, ALTCAT_1:21
.= G2 . [(f * ff),[bb,b]] by A40, A42, A52, A53, A58
.= G2 . (G1 . x) by A35, A37, A50, A51, A56, A57
.= (G2 * G1) . x by FUNCT_2:15 ; :: thesis:

end;

then G3 = G2 * G1 ;
hence H₂(a,c,g * f) = g9 * f9 by A31, A32, A36, A41, A46, A48, A49, Th36; :: thesis:

end;

A59: for a being Object of A
for a9 being Object of (Concretized A) st a9 = H₁(a) holds
H₂(a,a, idm a) = idm a9

proof

let a be Object of A; :: thesis:
let a9 be Object of (Concretized A); :: thesis:
assume A60: a9 = a ; :: thesis:
[a,a] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider c, b being Object of A, f being Morphism of c,b, G being Function of ((Concretized A) -carrier_of c),((Concretized A) -carrier_of b) such that
A61: [a,a] = [c,b] and
A62: idm a = f and
A63: (F . [a,a]) . (idm a) = G and
A64: for d being Object of A
for g being Morphism of d,c st <^d,c^> <> {} holds
G . [g,[d,c]] = [(f * g),[d,b]] by A22;
A65: idm a9 = id (the_carrier_of a9) by Def10;
A66: a = c by A61, XTUPLE_0:1;
A67: a = b by A61, XTUPLE_0:1;

now :: thesis:

let x be Element of the_carrier_of a9; :: thesis:
consider bb being Object of A, ff being Morphism of bb,a such that
A68: <^bb,a^> <> {} and
A69: x = [ff,[bb,a]] by A60, Th43;
thus G . x = [((idm a) * ff),[bb,a]] by A62, A64, A66, A67, A68, A69
.= x by A68, A69, ALTCAT_1:20
.= (id (the_carrier_of a9)) . x ; :: thesis:

end;

hence H₂(a,a, idm a) = idm a9 by A60, A63, A65, A66, A67, FUNCT_2:63; :: thesis:

end;

consider FF being strict covariant Functor of A, Concretized A such that
A70: for a being Object of A holds FF . a = H₁(a) and
A71: for a, b being Object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds FF . f = H₂(a,b,f) from YELLOW18:sch 8(A14, A23, A25, A59);
take FF ; :: thesis:
thus for a being Object of A holds FF . a = a by A70; :: thesis:
let a, b be Object of A; :: thesis:
assume A72: <^a,b^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
[a,b] in [: the carrier of A, the carrier of A:] by ZFMISC_1:def 2;
then consider a9, b9 being Object of A, f9 being Morphism of a9,b9, G being Function of ((Concretized A) -carrier_of a9),((Concretized A) -carrier_of b9) such that
A73: [a,b] = [a9,b9] and
A74: f = f9 and
A75: (F . [a,b]) . f = G and
A76: for c being Object of A
for g being Morphism of c,a9 st <^c,a9^> <> {} holds
G . [g,[c,a9]] = [(f9 * g),[c,b9]] by A22, A72;
A77: G = FF . f by A71, A72, A75;
A78: a = a9 by A73, XTUPLE_0:1;
b = b9 by A73, XTUPLE_0:1;
hence (FF . f) . [(idm a),[a,a]] = [(f * (idm a)),[a,b]] by A74, A76, A77, A78
.= [f,[a,b]] by A72, ALTCAT_1:def 17 ;
:: thesis: