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

let i, x be set ; :: thesis:
assume i in [:the carrier of A,the carrier of A:] ; :: thesis:
then consider a, b being set 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 by A16, A17;
assume A19: x in the Arrows of A . i ; :: thesis:
then reconsider f = x as Morphism of , 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
for g being Morphism of , st <^c,a^> <> {} holds
G . [g,[c,a]] = [(f * g),[c,b]] by A18, A19, Th46;
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 set 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 st <^a,b^> <> {} holds
for f being Morphism of , holds H₂(a,b,f) in the Arrows of (Concretized A) . H₁(a),H₁(b)

proof

let a, b be object of ; :: thesis:
assume A24: <^a,b^> <> {} ; :: thesis:
let f be Morphism of ,; :: 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 st <^a,b^> <> {} & <^b,c^> <> {} holds
for f being Morphism of ,
for g being Morphism of ,
for a', b', c' being object of st a' = H₁(a) & b' = H₁(b) & c' = H₁(c) holds
for f' being Morphism of ,
for g' being Morphism of , st f' = H₂(a,b,f) & g' = H₂(b,c,g) holds
H₂(a,c,g * f) = g' * f'

proof

let a, b, c be object of ; :: thesis:
assume that
A26: <^a,b^> <> {} and
A27: <^b,c^> <> {} ; :: thesis:
let f be Morphism of ,; :: thesis:
let g be Morphism of ,; :: thesis:
let a', b', c' be object of ; :: thesis:
assume that
A28: a' = a and
A29: b' = b and
A30: c' = c ; :: thesis:
let f' be Morphism of ,; :: thesis:
let g' be Morphism of ,; :: thesis:
assume that
A31: f' = (F . [a,b]) . f and
A32: g' = (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 , f1 being Morphism of ,, 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
for g being Morphism of , 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 , g2 being Morphism of ,, 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
for g being Morphism of , st <^c,b2^> <> {} holds
G2 . [g,[c,b2]] = [(g2 * g),[c,c2]] by A22, A27;
A43: <^a,c^> <> {} by A26, A27, ALTCAT_1:def 4;
[a,c] in [:the carrier of A,the carrier of A:] by ZFMISC_1:def 2;
then consider a3, c3 being object of , h3 being Morphism of ,, 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
for g being Morphism of , st <^c,a3^> <> {} holds
G3 . [g,[c,a3]] = [(h3 * g),[c,c3]] by A22, A43;
A48: (F . [a,b]) . f in <^a',b'^> by A22, A26, A28, A29, A33;
A49: (F . [b,c]) . g in <^b',c'^> by A22, A27, A29, A30, A38;
A50: a = a1 by A34, ZFMISC_1:33;
A51: b = b1 by A34, ZFMISC_1:33;
A52: b = b2 by A39, ZFMISC_1:33;
A53: c = c2 by A39, ZFMISC_1:33;
A54: a = a3 by A44, ZFMISC_1:33;
A55: c = c3 by A44, ZFMISC_1:33;
reconsider G1 = G1 as Function of (Concretized A) -carrier_of a,(Concretized A) -carrier_of b by A34, A50, ZFMISC_1:33;
reconsider G2 = G2 as Function of (Concretized A) -carrier_of b,(Concretized A) -carrier_of c by A39, A52, ZFMISC_1:33;
reconsider G3 = G3 as Function of (Concretized A) -carrier_of a,(Concretized A) -carrier_of c by A44, A54, ZFMISC_1:33;

now

let x be Element of (Concretized A) -carrier_of a; :: thesis:
consider bb being object of , ff being Morphism of , such that
A56: <^bb,a^> <> {} and
A57: x = [ff,[bb,a]] by Th45;
A58: <^bb,b^> <> {} by A26, A56, ALTCAT_1:def 4;
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:25
.= 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:21 ; :: thesis:

end;

then G3 = G2 * G1 by FUNCT_2:113;
hence H₂(a,c,g * f) = g' * f' by A31, A32, A36, A41, A46, A48, A49, Th38; :: thesis:

end;

A59: for a being object of
for a' being object of st a' = H₁(a) holds
H₂(a,a, idm a) = idm a'

proof

let a be object of ; :: thesis:
let a' be object of ; :: thesis:
assume A60: a' = 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 , f being Morphism of ,, 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
for g being Morphism of , st <^d,c^> <> {} holds
G . [g,[d,c]] = [(f * g),[d,b]] by A22;
A65: idm a' = id (the_carrier_of a') by Def10;
A66: a = c by A61, ZFMISC_1:33;
A67: a = b by A61, ZFMISC_1:33;

now

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

end;

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

end;

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