thus ( F₄() is subcategory of F₁() & F₅() is subcategory of F₂() ) ; :: according to YELLOW20:def 4 :: thesis:
A4: the carrier of F₄() c= the carrier of F₁() by ALTCAT_2:def 11;
deffunc H₁( object of F₄()) -> Element of the carrier of F₂() = (F₃() | F₄()) . $1;
deffunc H₂( object of F₄(), object of F₄(), Morphism of $1,$2) -> Element of <^((F₃() | F₄()) . $1),((F₃() | F₄()) . $2)^> = (F₃() | F₄()) . $3;

A5: now

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

end;

A6: now

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 c = a, d = b as object of F₁() by A4;
reconsider a' = (F₃() | F₄()) . a, b' = (F₃() | F₄()) . b as object of F₅() by A5;
let f be Morphism of a,b; :: thesis:
A8: ( <^a,b^> c= <^c,d^> & f in <^a,b^> ) by A7, ALTCAT_2:32;
then reconsider g = f as Morphism of c,d ;
( (F₃() | F₄()) . a = F₃() . c & (F₃() | F₄()) . b = F₃() . d & (F₃() | F₄()) . f = F₃() . g ) by A7, Th29, Th30;
then (F₃() | F₄()) . f in <^a',b'^> by A3, A8;
hence H₂(a,b,f) in the Arrows of F₅() . H₁(a),H₁(b) ; :: thesis:

end;

A9: now

let a, b, c be object of F₄(); :: thesis:
assume A10: ( <^a,b^> <> {} & <^b,c^> <> {} ) ; :: thesis:
( a in the carrier of F₄() & b in the carrier of F₄() & c in the carrier of F₄() ) ;
then reconsider a1 = a, b1 = b, c1 = c as object of F₁() by A4;
let f be Morphism of a,b; :: thesis:
let g be Morphism of b,c; :: thesis:
let a', b', c' be object of F₅(); :: thesis:
assume A11: ( a' = H₁(a) & b' = H₁(b) & c' = H₁(c) ) ; :: thesis:
let f' be Morphism of a',b'; :: thesis:
let g' be Morphism of b',c'; :: thesis:
assume A12: ( f' = H₂(a,b,f) & g' = H₂(b,c,g) ) ; :: thesis:
A13: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A10, ALTCAT_2:32;
then reconsider f1 = f as Morphism of a1,b1 ;
A14: ( <^b,c^> c= <^b1,c1^> & g in <^b,c^> ) by A10, ALTCAT_2:32;
then reconsider g1 = g as Morphism of b1,c1 ;
A15: <^a,c^> <> {} by A10, ALTCAT_1:def 4;
A16: g * f = g1 * f1 by A10, ALTCAT_2:33;
A17: ( a' = F₃() . a1 & b' = F₃() . b1 & c' = F₃() . c1 ) by A11, Th29;
A18: ( (F₃() | F₄()) . (g * f) = F₃() . (g1 * f1) & f' = F₃() . f1 & g' = F₃() . g1 ) by A10, A12, A15, A16, Th30;
then A19: ( f' in <^a',b'^> & g' in <^b',c'^> ) by A3, A13, A14, A17;
thus H₂(a,c,g * f) = (F₃() . g1) * (F₃() . f1) by A13, A14, A18, FUNCTOR0:def 24
.= g' * f' by A17, A18, A19, ALTCAT_2:33 ; :: thesis:

end;

A20: now

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

end;

consider G being strict covariant Functor of F₄(),F₅() such that
A22: for a being object of F₄() holds G . a = H₁(a) and
A23: 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(A5, A6, A9, A20);
take G ; :: thesis:
A24: ( F₃() is injective & F₃() is surjective ) by A1, FUNCTOR0:def 36;
then A25: ( F₃() is one-to-one & F₃() is faithful & F₃() is surjective ) by FUNCTOR0:def 34;

A26: 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 A4;
assume H₁(a) = H₁(b) ; :: thesis:
then F₃() . a1 = (F₃() | F₄()) . b by Th29
.= F₃() . b1 by Th29 ;
hence a = b by A25, Th32; :: thesis:

end;

A27: now

let a, b be object of F₄(); :: thesis:
assume A28: <^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 A4;
let f, g be Morphism of a,b; :: thesis:
A29: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> & g in <^a,b^> ) by A28, ALTCAT_2:32;
then reconsider f1 = f, g1 = g as Morphism of a1,b1 ;
assume H₂(a,b,f) = H₂(a,b,g) ; :: thesis:
then F₃() . f1 = (F₃() | F₄()) . g by A28, Th30
.= F₃() . g1 by A28, Th30 ;
hence f = g by A25, A29, Th33; :: thesis:

end;

A30: 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) )

proof

let a, b be object of F₅(); :: thesis:
assume A31: <^a,b^> <> {} ; :: thesis:
( a in the carrier of F₅() & b in the carrier of F₅() & the carrier of F₅() c= the carrier of F₂() ) by ALTCAT_2:def 11;
then reconsider a1 = a, b1 = b as object of F₂() ;
let f be Morphism of a,b; :: thesis:
A32: ( <^a,b^> c= <^a1,b1^> & f in <^a,b^> ) by A31, 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
A33: ( a1 = F₃() . c1 & b1 = F₃() . d1 & <^c1,d1^> <> {} & f1 = F₃() . g1 ) by A24, A32, Th34;
reconsider c = c1, d = d1 as object of F₄() by A2, A33;
A34: g1 in <^c,d^> by A3, A31, A33;
reconsider g = g1 as Morphism of c,d by A3, A31, A33;
take c ; :: thesis:
take d ; :: thesis:
take g ; :: thesis:
thus ( a = H₁(c) & b = H₁(d) & <^c,d^> <> {} & f = H₂(c,d,g) ) by A33, A34, Th29, Th30; :: thesis:

end;

thus G is bijective from YELLOW18:sch 10(A22, A23, A26, A27, A30); :: thesis:

hereby :: thesis:

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

end;

let b, c be object of F₄(); :: thesis:
let b1, c1 be object of F₁(); :: thesis:
assume A36: ( <^b,c^> <> {} & b1 = b & c1 = c ) ; :: thesis:
let f be Morphism of b,c; :: thesis:
let f1 be Morphism of b1,c1; :: thesis:
assume A37: f = f1 ; :: thesis:
A38: ( <^b,c^> c= <^b1,c1^> & f in <^b,c^> ) by A36, ALTCAT_2:32;
then A39: <^(F₃() . b1),(F₃() . c1)^> <> {} by FUNCTOR0:def 19;
thus G . f = (F₃() | F₄()) . f by A23, A36
.= F₃() . f1 by A36, A37, Th30
.= (Morph-Map F₃(),b1,c1) . f1 by A38, A39, FUNCTOR0:def 16 ; :: thesis: