consider X being set such that
A4: for x being object holds
( x in X iff ( x in the carrier of F₁() & P₁[x] ) ) from XBOOLE_0:sch 1();
reconsider X = X as non empty set by A1, A4;
A5: X c= the carrier of F₁() by A4;
deffunc H₁( set , set ) -> set = the Arrows of F₁() . ($1,$2);
deffunc H₂( set , set , set , set , set ) -> set = ( the Comp of F₁() . ($1,$2,$3)) . ($5,$4);

let a, b, c be Element of X; :: thesis:
let f, g be set ; :: thesis:
assume that
A7: f in H₁(a,b) and
A8: P₂[a,b,f] and
A9: g in H₁(b,c) and
A10: P₂[b,c,g] ; :: thesis:
reconsider a9 = a, b9 = b, c9 = c as Object of F₁() by A4;
A11: H₁(a,b) = <^a9,b9^> ;
reconsider f9 = f as Morphism of a9,b9 by A7;
A12: H₁(b,c) = <^b9,c9^> ;
reconsider g9 = g as Morphism of b9,c9 by A9;
A13: H₂(a,b,c,f,g) = g9 * f9 by A7, A9, ALTCAT_1:def 8;
<^a9,c9^> <> {} by A7, A9, A11, A12, ALTCAT_1:def 2;
hence H₂(a,b,c,f,g) in H₁(a,c) by A13; :: thesis:
A14: P₁[a9] by A4;
A15: P₁[b9] by A4;
P₁[c9] by A4;
hence P₂[a,c,H₂(a,b,c,f,g)] by A2, A7, A8, A9, A10, A13, A14, A15; :: thesis:

end;

A16: now :: thesis:

let a, b, c, d be Element of X; :: thesis:
let f, g, h be set ; :: thesis:
assume that
A17: f in H₁(a,b) and
P₂[a,b,f] and
A18: g in H₁(b,c) and
P₂[b,c,g] and
A19: h in H₁(c,d) and
P₂[c,d,h] ; :: thesis:
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Object of F₁() by A4;
A20: H₁(a,b) = <^a9,b9^> ;
reconsider f9 = f as Morphism of a9,b9 by A17;
A21: H₁(b,c) = <^b9,c9^> ;
reconsider g9 = g as Morphism of b9,c9 by A18;
A22: H₁(c,d) = <^c9,d9^> ;
reconsider h9 = h as Morphism of c9,d9 by A19;
A23: <^a9,c9^> <> {} by A17, A18, A20, A21, ALTCAT_1:def 2;
A24: <^b9,d9^> <> {} by A18, A19, A21, A22, ALTCAT_1:def 2;
thus H₂(a,c,d,H₂(a,b,c,f,g),h) = H₂(a9,c9,d9,g9 * f9,h) by A17, A18, ALTCAT_1:def 8
.= h9 * (g9 * f9) by A19, A23, ALTCAT_1:def 8
.= (h9 * g9) * f9 by A17, A18, A19, ALTCAT_1:21
.= H₂(a,b,d,f,h9 * g9) by A17, A24, ALTCAT_1:def 8
.= H₂(a,b,d,f,H₂(b,c,d,g,h)) by A18, A19, ALTCAT_1:def 8 ; :: thesis:

end;

A25: now :: thesis:

let a be Element of X; :: thesis:
reconsider b = a as Object of F₁() by A4;
reconsider f = idm b as set ;
take f = f; :: thesis:
P₁[b] by A4;
hence ( f in H₁(a,a) & P₂[a,a,f] ) by A3; :: thesis:
let c be Element of X; :: thesis:
let g be set ; :: thesis:
assume that
A26: g in H₁(a,c) and
P₂[a,c,g] ; :: thesis:
reconsider d = c as Object of F₁() by A4;
reconsider g9 = g as Morphism of b,d by A26;
thus H₂(a,a,c,f,g) = g9 * (idm b) by A26, ALTCAT_1:def 8
.= g by A26, ALTCAT_1:def 17 ; :: thesis:

end;

A27: now :: thesis:

let a be Element of X; :: thesis:
reconsider b = a as Object of F₁() by A4;
reconsider f = idm b as set ;
take f = f; :: thesis:
P₁[b] by A4;
hence ( f in H₁(a,a) & P₂[a,a,f] ) by A3; :: thesis:
let c be Element of X; :: thesis:
let g be set ; :: thesis:
assume that
A28: g in H₁(c,a) and
P₂[c,a,g] ; :: thesis:
reconsider d = c as Object of F₁() by A4;
reconsider g9 = g as Morphism of d,b by A28;
thus H₂(c,a,a,g,f) = (idm b) * g9 by A28, ALTCAT_1:def 8
.= g by A28, ALTCAT_1:20 ; :: thesis:

end;

consider C being strict category such that
A29: the carrier of C = X and
A30: for a, b being Object of C
for f being set holds
( f in <^a,b^> iff ( f in H₁(a,b) & P₂[a,b,f] ) ) and
A31: 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 6(A6, A16, A25, A27);
C is SubCatStr of F₁()

proof

thus the carrier of C c= the carrier of F₁() by A5, A29; :: according to ALTCAT_2:def 11 :: thesis:
thus [: the carrier of C, the carrier of C:] c= [: the carrier of F₁(), the carrier of F₁():] by A5, A29, ZFMISC_1:96; :: according to ALTCAT_2:def 2 :: thesis:

hereby :: thesis:

let i be set ; :: thesis:
assume i in [: the carrier of C, the carrier of C:] ; :: thesis:
then consider a, b being object such that
A32: a in the carrier of C and
A33: b in the carrier of C and
A34: [a,b] = i by ZFMISC_1:def 2;
reconsider a = a, b = b as Object of C by A32, A33;
A35: the Arrows of C . i = <^a,b^> by A34;
A36: the Arrows of F₁() . i = the Arrows of F₁() . (a,b) by A34;
thus the Arrows of C . i c= the Arrows of F₁() . i by A30, A35, A36; :: thesis:

end;

thus [: the carrier of C, the carrier of C, the carrier of C:] c= [: the carrier of F₁(), the carrier of F₁(), the carrier of F₁():] by A5, A29, MCART_1:73; :: according to ALTCAT_2:def 2 :: thesis:
let i be set ; :: thesis:
assume i in [: the carrier of C, the carrier of C, the carrier of C:] ; :: thesis:
then consider a, b, c being object such that
A37: a in the carrier of C and
A38: b in the carrier of C and
A39: c in the carrier of C and
A40: [a,b,c] = i by MCART_1:68;
reconsider a = a, b = b, c = c as Object of C by A37, A38, A39;
reconsider a9 = a, b9 = b, c9 = c as Object of F₁() by A4, A29;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the Comp of C . i ; :: thesis:
then A41: x in the Comp of C . (a,b,c) by A40, MULTOP_1:def 1;
then consider gf, h being object such that
A42: x = [gf,h] and
A43: gf in [:( the Arrows of C . (b,c)),( the Arrows of C . (a,b)):] and
A44: h in the Arrows of C . (a,c) by RELSET_1:2;
consider g, f being object such that
A45: g in the Arrows of C . (b,c) and
A46: f in the Arrows of C . (a,b) and
A47: [g,f] = gf by A43, ZFMISC_1:def 2;
reconsider f = f as Morphism of a,b by A46;
reconsider g = g as Morphism of b,c by A45;
reconsider h = h as Morphism of a,c by A44;
A48: the Comp of F₁() . (a9,b9,c9) = the Comp of F₁() . i by A40, MULTOP_1:def 1;
A49: g in the Arrows of F₁() . (b9,c9) by A30, A45;
A50: f in the Arrows of F₁() . (a9,b9) by A30, A46;
A51: h = ( the Comp of C . (a,b,c)) . (g,f) by A41, A42, A47, FUNCT_1:1
.= g * f by A45, A46, ALTCAT_1:def 8
.= ( the Comp of F₁() . (a9,b9,c9)) . (g,f) by A31, A45, A46 ;
h in the Arrows of F₁() . (a9,c9) by A30, A44;
then dom ( the Comp of F₁() . (a9,b9,c9)) = [:( the Arrows of F₁() . (b9,c9)),( the Arrows of F₁() . (a9,b9)):] by FUNCT_2:def 1;
then gf in dom ( the Comp of F₁() . (a9,b9,c9)) by A47, A49, A50, ZFMISC_1:def 2;
hence x in the Comp of F₁() . i by A42, A47, A48, A51, FUNCT_1:def 2; :: thesis:

end;

then reconsider C = C as non empty SubCatStr of F₁() ;
for o being Object of C
for o9 being Object of F₁() st o = o9 holds
idm o9 in <^o,o^>

proof

let a be Object of C; :: thesis:
let b be Object of F₁(); :: thesis:
assume A52: a = b ; :: thesis:
then P₁[b] by A4, A29;
then P₂[b,b, idm b] by A3;
hence idm b in <^a,a^> by A30, A52; :: thesis:

end;

then reconsider C = C as non empty strict subcategory of F₁() by ALTCAT_2:def 14;
take C ; :: thesis:
thus for a being Object of F₁() holds
( a is Object of C iff P₁[a] ) by A4, A29; :: thesis:
let a, b be Object of F₁(); :: thesis:
let a9, b9 be Object of C; :: thesis:
assume that
A53: a9 = a and
A54: b9 = b and
A55: <^a,b^> <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
thus ( f in <^a9,b9^> iff P₂[a,b,f] ) by A30, A53, A54, A55; :: thesis: