deffunc H₁( object of F₄(), object of F₄(), Morphism of $1,$2) -> M2(<^((F₃() | F₄()) . $1),((F₃() | F₄()) . $2)^>) = (F₃() | F₄()) . $3;
deffunc H₂( object of F₄()) -> M2(the carrier of F₂()) = (F₃() | F₄()) . $1;
A4: ( F₃() is injective & F₃() is surjective ) by A1, FUNCTOR0:def 36;
A5: for a, b being object of F₅() st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of F₄() ex g being Morphism of c,d st
( a = H₂(c) & b = H₂(d) & <^c,d^> <> {} & f = H₁(c,d,g) )

A6: the carrier of F₅() c= the carrier of F₂() by ALTCAT_2:def 11;
let a, b be object of F₅(); :: thesis:
assume A7: <^a,b^> <> {} ; :: thesis:
( a in the carrier of F₅() & b in the carrier of F₅() ) ;
then reconsider a1 = a, b1 = b as object of F₂() by A6;
let f be Morphism of a,b; :: thesis:
A8: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A7, ALTCAT_2:32;
then reconsider f1 = f as Morphism of a1,b1 ;
consider c1, d1 being object of F₁(), g1 being Morphism of c1,d1 such that
A9: ( a1 = F₃() . c1 & b1 = F₃() . d1 ) and
A10: <^c1,d1^> <> {} and
A11: f1 = F₃() . g1 by A4, A8, Th34;
reconsider c = c1, d = d1 as object of F₄() by A2, A9;
reconsider g = g1 as Morphism of c,d by A3, A7, A9, A10, A11;
take c ; :: thesis:
take d ; :: thesis:
take g ; :: thesis:
g1 in <^c,d^> by A3, A7, A9, A10, A11;
hence ( a = H₂(c) & b = H₂(d) & <^c,d^> <> {} & f = H₁(c,d,g) ) by A9, A11, Th29, Th30; :: thesis:

end;

A13: now

let a be object of F₄(); :: thesis:
a in the carrier of F₄() ;
then reconsider b = a as object of F₁() by A12;
(F₃() | F₄()) . a = F₃() . b by Th29;
hence H₂(a) is object of F₅() by A2; :: thesis:

end;

A14: now

let a, b be object of F₄(); :: thesis:
assume A15: <^a,b^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
( a in the carrier of F₄() & b in the carrier of F₄() ) ;
then reconsider c = a, d = b as object of F₁() by A12;
A16: ( <^a,b^> c= <^c,d^> & f in <^a,b^> ) by A15, ALTCAT_2:32;
then reconsider g = f as Morphism of c,d ;
reconsider a9 = (F₃() | F₄()) . a, b9 = (F₃() | F₄()) . b as object of F₅() by A13;
A17: ( (F₃() | F₄()) . a = F₃() . c & (F₃() | F₄()) . b = F₃() . d ) by Th29;
(F₃() | F₄()) . f = F₃() . g by A15, Th30;
then (F₃() | F₄()) . f in <^a9,b9^> by A3, A16, A17;
hence H₁(a,b,f) in the Arrows of F₅() . H₂(a),H₂(b) ; :: thesis:

end;

A19: now

let a, b be object of F₄(); :: thesis:
assume A20: <^a,b^> <> {} ; :: thesis:
( a in the carrier of F₄() & b in the carrier of F₄() ) ;
then reconsider a1 = a, b1 = b as object of F₁() by A12;
let f, g be Morphism of a,b; :: thesis:
A21: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A20, ALTCAT_2:32;
g in <^a,b^> by A20;
then reconsider f1 = f, g1 = g as Morphism of a1,b1 by A21;
assume H₁(a,b,f) = H₁(a,b,g) ; :: thesis:
then F₃() . f1 = (F₃() | F₄()) . g by A20, Th30
.= F₃() . g1 by A20, Th30 ;
hence f = g by A18, A21, Th33; :: thesis:

end;

A22: now

let a, b, c be object of F₄(); :: thesis:
assume that
A23: <^a,b^> <> {} and
A24: <^b,c^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
let g be Morphism of b,c; :: thesis:
A25: c in the carrier of F₄() ;
( a in the carrier of F₄() & b in the carrier of F₄() ) ;
then reconsider a1 = a, b1 = b, c1 = c as object of F₁() by A12, A25;
let a9, b9, c9 be object of F₅(); :: thesis:
assume that
A26: a9 = H₂(a) and
A27: b9 = H₂(b) and
A28: c9 = H₂(c) ; :: thesis:
let f9 be Morphism of a9,b9; :: thesis:
let g9 be Morphism of b9,c9; :: thesis:
assume that
A29: f9 = H₁(a,b,f) and
A30: g9 = H₁(b,c,g) ; :: thesis:
A31: b9 = F₃() . b1 by A27, Th29;
A32: ( <^b,c^> c= <^b1,c1^> & g in <^b,c^> ) by A24, ALTCAT_2:32;
then reconsider g1 = g as Morphism of b1,c1 ;
A33: c9 = F₃() . c1 by A28, Th29;
A34: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A23, ALTCAT_2:32;
then reconsider f1 = f as Morphism of a1,b1 ;
A35: a9 = F₃() . a1 by A26, Th29;
A36: g9 = F₃() . g1 by A24, A30, Th30;
then A37: g9 in <^b9,c9^> by A3, A32, A31, A33;
A38: f9 = F₃() . f1 by A23, A29, Th30;
then A39: f9 in <^a9,b9^> by A3, A34, A35, A31;
( <^a,c^> <> {} & g * f = g1 * f1 ) by A23, A24, ALTCAT_1:def 4, ALTCAT_2:33;
then (F₃() | F₄()) . (g * f) = F₃() . (g1 * f1) by Th30;
hence H₁(a,c,g * f) = (F₃() . g1) * (F₃() . f1) by A34, A32, FUNCTOR0:def 24
.= g9 * f9 by A35, A31, A33, A38, A36, A39, A37, ALTCAT_2:33 ;
:: thesis:

end;

A40: now

let a be object of F₄(); :: thesis:
let a9 be object of F₅(); :: thesis:
assume A41: a9 = H₂(a) ; :: thesis:
a in the carrier of F₄() ;
then reconsider a1 = a as object of F₁() by A12;
thus H₁(a,a, idm a) = F₃() . (idm a1) by Th30, ALTCAT_2:35
.= idm (F₃() . a1) by FUNCTOR2:2
.= idm a9 by A41, Th29, ALTCAT_2:35 ; :: thesis:

end;

consider G being strict covariant Functor of F₄(),F₅() such that
A42: for a being object of F₄() holds G . a = H₂(a) and
A43: for a, b being object of F₄() st <^a,b^> <> {} holds
for f being Morphism of a,b holds G . f = H₁(a,b,f) from YELLOW18:sch 8(A13, A14, A22, A40);
take G ; :: thesis:

A44: now

let a, b be object of F₄(); :: thesis:
( a in the carrier of F₄() & b in the carrier of F₄() ) ;
then reconsider a1 = a, b1 = b as object of F₁() by A12;
assume H₂(a) = H₂(b) ; :: thesis:
then F₃() . a1 = (F₃() | F₄()) . b by Th29
.= F₃() . b1 by Th29 ;
hence a = b by A18, Th32; :: thesis:

end;

let a be object of F₄(); :: thesis:
let a1 be object of F₁(); :: thesis:
assume A45: a = a1 ; :: thesis:
thus G . a = (F₃() | F₄()) . a by A42
.= F₃() . a1 by A45, Th29 ; :: thesis:

end;

let b, c be object of F₄(); :: thesis:
let b1, c1 be object of F₁(); :: thesis:
assume that
A46: <^b,c^> <> {} and
A47: ( b1 = b & c1 = c ) ; :: thesis:
let f be Morphism of b,c; :: thesis:
let f1 be Morphism of b1,c1; :: thesis:
assume A48: f = f1 ; :: thesis:
A49: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A46, A47, ALTCAT_2:32;
then A50: <^(F₃() . b1),(F₃() . c1)^> <> {} by FUNCTOR0:def 19;
thus G . f = (F₃() | F₄()) . f by A43, A46
.= F₃() . f1 by A46, A47, A48, Th30
.= (Morph-Map F₃(),b1,c1) . f1 by A49, A50, FUNCTOR0:def 16 ; :: thesis: