consider X being set such that
A4: for x being set holds
( x in X iff ( x in the carrier of F1() & P1[x] ) ) from XBOOLE_0:sch 1();
 reconsider X = X as non empty set by A1, A4;
A5: X c= the carrier of F1()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in the carrier of F1() )
thus ( not x in X or x in the carrier of F1() ) by A4; :: thesis: verum
end;
deffunc H1( set , set ) -> set = the Arrows of F1() . $1,$2;
deffunc H2( set , set , set , set , set ) -> set = (the Comp of F1() . $1,$2,$3) . $5,$4;
A6: now
let a, b, c be Element of X; :: thesis: for f, g being set st f in H1(a,b) & P2[a,b,f] & g in H1(b,c) & P2[b,c,g] holds
( H2(a,b,c,f,g) in H1(a,c) & P2[a,c,H2(a,b,c,f,g)] )
let f, g be set ; :: thesis: ( f in H1(a,b) & P2[a,b,f] & g in H1(b,c) & P2[b,c,g] implies ( H2(a,b,c,f,g) in H1(a,c) & P2[a,c,H2(a,b,c,f,g)] ) )
assume that
A7: f in H1(a,b) and
A8: P2[a,b,f] and
A9: g in H1(b,c) and
A10: P2[b,c,g] ; :: thesis: ( H2(a,b,c,f,g) in H1(a,c) & P2[a,c,H2(a,b,c,f,g)] )
reconsider a9 = a, b9 = b, c9 = c as object of F1() by A4;
A11: H1(a,b) = <^a9,b9^> ;
reconsider f9 = f as Morphism of a9,b9 by A7;
A12: H1(b,c) = <^b9,c9^> ;
reconsider g9 = g as Morphism of b9,c9 by A9;
A13: H2(a,b,c,f,g) = g9 * f9 by A7, A9, ALTCAT_1:def 10;
<^a9,c9^> <> {} by A7, A9, A11, A12, ALTCAT_1:def 4;
hence H2(a,b,c,f,g) in H1(a,c) by A13; :: thesis: P2[a,c,H2(a,b,c,f,g)]
A14: P1[a9] by A4;
A15: P1[b9] by A4;
P1[c9] by A4;
hence P2[a,c,H2(a,b,c,f,g)] by A2, A7, A8, A9, A10, A13, A14, A15; :: thesis: verum
end;
A16: now
let a, b, c, d be Element of X; :: thesis: for f, g, h being set st f in H1(a,b) & P2[a,b,f] & g in H1(b,c) & P2[b,c,g] & h in H1(c,d) & P2[c,d,h] holds
H2(a,c,d,H2(a,b,c,f,g),h) = H2(a,b,d,f,H2(b,c,d,g,h))
let f, g, h be set ; :: thesis: ( f in H1(a,b) & P2[a,b,f] & g in H1(b,c) & P2[b,c,g] & h in H1(c,d) & P2[c,d,h] implies H2(a,c,d,H2(a,b,c,f,g),h) = H2(a,b,d,f,H2(b,c,d,g,h)) )
assume that
A17: f in H1(a,b) and
P2[a,b,f] and
A18: g in H1(b,c) and
P2[b,c,g] and
A19: h in H1(c,d) and
P2[c,d,h] ; :: thesis: H2(a,c,d,H2(a,b,c,f,g),h) = H2(a,b,d,f,H2(b,c,d,g,h))
reconsider a9 = a, b9 = b, c9 = c, d9 = d as object of F1() by A4;
A20: H1(a,b) = <^a9,b9^> ;
reconsider f9 = f as Morphism of a9,b9 by A17;
A21: H1(b,c) = <^b9,c9^> ;
reconsider g9 = g as Morphism of b9,c9 by A18;
A22: H1(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 4;
A24: <^b9,d9^> <> {} by A18, A19, A21, A22, ALTCAT_1:def 4;
thus H2(a,c,d,H2(a,b,c,f,g),h) = H2(a9,c9,d9,g9 * f9,h) by A17, A18, ALTCAT_1:def 10
.= h9 * (g9 * f9) by A19, A23, ALTCAT_1:def 10
.= (h9 * g9) * f9 by A17, A18, A19, ALTCAT_1:25
.= H2(a,b,d,f,h9 * g9) by A17, A24, ALTCAT_1:def 10
.= H2(a,b,d,f,H2(b,c,d,g,h)) by A18, A19, ALTCAT_1:def 10 ; :: thesis: verum
end;
A25: now
let a be Element of X; :: thesis: ex f being set st
( f in H1(a,a) & P2[a,a,f] & ( for c being Element of X
for g being set st g in H1(a,c) & P2[a,c,g] holds
H2(a,a,c,f,g) = g ) )
reconsider b = a as object of F1() by A4;
reconsider f = idm b as set ;
take f = f; :: thesis: ( f in H1(a,a) & P2[a,a,f] & ( for c being Element of X
for g being set st g in H1(a,c) & P2[a,c,g] holds
H2(a,a,c,f,g) = g ) )
P1[b] by A4;
hence ( f in H1(a,a) & P2[a,a,f] ) by A3; :: thesis: for c being Element of X
for g being set st g in H1(a,c) & P2[a,c,g] holds
H2(a,a,c,f,g) = g
let c be Element of X; :: thesis: for g being set st g in H1(a,c) & P2[a,c,g] holds
H2(a,a,c,f,g) = g
let g be set ; :: thesis: ( g in H1(a,c) & P2[a,c,g] implies H2(a,a,c,f,g) = g )
assume that
A26: g in H1(a,c) and
P2[a,c,g] ; :: thesis: H2(a,a,c,f,g) = g
reconsider d = c as object of F1() by A4;
reconsider g9 = g as Morphism of b,d by A26;
thus H2(a,a,c,f,g) = g9 * (idm b) by A26, ALTCAT_1:def 10
.= g by A26, ALTCAT_1:def 19 ; :: thesis: verum
end;
A27: now
let a be Element of X; :: thesis: ex f being set st
( f in H1(a,a) & P2[a,a,f] & ( for c being Element of X
for g being set st g in H1(c,a) & P2[c,a,g] holds
H2(c,a,a,g,f) = g ) )
reconsider b = a as object of F1() by A4;
reconsider f = idm b as set ;
take f = f; :: thesis: ( f in H1(a,a) & P2[a,a,f] & ( for c being Element of X
for g being set st g in H1(c,a) & P2[c,a,g] holds
H2(c,a,a,g,f) = g ) )
P1[b] by A4;
hence ( f in H1(a,a) & P2[a,a,f] ) by A3; :: thesis: for c being Element of X
for g being set st g in H1(c,a) & P2[c,a,g] holds
H2(c,a,a,g,f) = g
let c be Element of X; :: thesis: for g being set st g in H1(c,a) & P2[c,a,g] holds
H2(c,a,a,g,f) = g
let g be set ; :: thesis: ( g in H1(c,a) & P2[c,a,g] implies H2(c,a,a,g,f) = g )
assume that
A28: g in H1(c,a) and
P2[c,a,g] ; :: thesis: H2(c,a,a,g,f) = g
reconsider d = c as object of F1() by A4;
reconsider g9 = g as Morphism of d,b by A28;
thus H2(c,a,a,g,f) = (idm b) * g9 by A28, ALTCAT_1:def 10
.= g by A28, ALTCAT_1:24 ; :: thesis: verum
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 H1(a,b) & P2[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 = H2(a,b,c,f,g) from YELLOW18:sch 6(A6, A16, A25, A27);
 C is SubCatStr of F1()
proof
thus the carrier of C c= the carrier of F1() by A5, A29; :: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of C cc= the Arrows of F1() & the Comp of C cc= the Comp of F1() )
thus [:the carrier of C,the carrier of C:] c= [:the carrier of F1(),the carrier of F1():] by A5, A29, ZFMISC_1:119; :: according to ALTCAT_2:def 2 :: thesis: ( ( for b1 being set holds
( not b1 in [:the carrier of C,the carrier of C:] or the Arrows of C . b1 c= the Arrows of F1() . b1 ) ) & the Comp of C cc= the Comp of F1() )
hereby :: thesis: the Comp of C cc= the Comp of F1()
let i be set ; :: thesis: ( i in [:the carrier of C,the carrier of C:] implies the Arrows of C . i c= the Arrows of F1() . i )
assume i in [:the carrier of C,the carrier of C:] ; :: thesis: the Arrows of C . i c= the Arrows of F1() . i
then consider a, b being set 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 F1() . i = the Arrows of F1() . a,b by A34;
thus the Arrows of C . i c= the Arrows of F1() . i :: thesis: verum
proof
let f be set ; :: according to TARSKI:def 3 :: thesis: ( not f in the Arrows of C . i or f in the Arrows of F1() . i )
thus ( not f in the Arrows of C . i or f in the Arrows of F1() . i ) by A30, A35, A36; :: thesis: verum
end;
end;
thus [:the carrier of C,the carrier of C,the carrier of C:] c= [:the carrier of F1(),the carrier of F1(),the carrier of F1():] by A5, A29, MCART_1:77; :: according to ALTCAT_2:def 2 :: thesis: for b1 being set holds
( not b1 in [:the carrier of C,the carrier of C,the carrier of C:] or the Comp of C . b1 c= the Comp of F1() . b1 )
let i be set ; :: thesis: ( not i in [:the carrier of C,the carrier of C,the carrier of C:] or the Comp of C . i c= the Comp of F1() . i )
assume i in [:the carrier of C,the carrier of C,the carrier of C:] ; :: thesis: the Comp of C . i c= the Comp of F1() . i
then consider a, b, c being set 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:72;
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 F1() by A4, A29;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Comp of C . i or x in the Comp of F1() . i )
assume x in the Comp of C . i ; :: thesis: x in the Comp of F1() . i
then A41: x in the Comp of C . a,b,c by A40, MULTOP_1:def 1;
then consider gf, h being set 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:6;
consider g, f being set 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 F1() . a9,b9,c9 = the Comp of F1() . i by A40, MULTOP_1:def 1;
A49: g in the Arrows of F1() . b9,c9 by A30, A45;
A50: f in the Arrows of F1() . a9,b9 by A30, A46;
A51: h = (the Comp of C . a,b,c) . g,f by A41, A42, A47, FUNCT_1:8
.= g * f by A45, A46, ALTCAT_1:def 10
.= (the Comp of F1() . a9,b9,c9) . g,f by A31, A45, A46 ;
h in the Arrows of F1() . a9,c9 by A30, A44;
then dom (the Comp of F1() . a9,b9,c9) = [:(the Arrows of F1() . b9,c9),(the Arrows of F1() . a9,b9):] by FUNCT_2:def 1;
then gf in dom (the Comp of F1() . a9,b9,c9) by A47, A49, A50, ZFMISC_1:def 2;
hence x in the Comp of F1() . i by A42, A47, A48, A51, FUNCT_1:def 4; :: thesis: verum
end;
then reconsider C = C as non empty SubCatStr of F1() ;
for o being object of C
for o9 being object of F1() st o = o9 holds
idm o9 in <^o,o^>
proof
let a be object of C; :: thesis: for o9 being object of F1() st a = o9 holds
idm o9 in <^a,a^>
let b be object of F1(); :: thesis: ( a = b implies idm b in <^a,a^> )
assume A52: a = b ; :: thesis: idm b in <^a,a^>
then P1[b] by A4, A29;
then P2[b,b, idm b] by A3;
hence idm b in <^a,a^> by A30, A52; :: thesis: verum
end;
then reconsider C = C as non empty strict subcategory of F1() by ALTCAT_2:def 14;
take C ; :: thesis: ( ( for a being object of F1() holds
( a is object of C iff P1[a] ) ) & ( for a, b being object of F1()
for a9, b9 being object of C st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] ) ) )
thus for a being object of F1() holds
( a is object of C iff P1[a] ) by A4, A29; :: thesis: for a, b being object of F1()
for a9, b9 being object of C st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] )
let a, b be object of F1(); :: thesis: for a9, b9 being object of C st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] )
let a9, b9 be object of C; :: thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] ) )
assume that
A53: a9 = a and
A54: b9 = b and
A55: <^a,b^> <> {} ; :: thesis: for f being Morphism of a,b holds
( f in <^a9,b9^> iff P2[a,b,f] )
let f be Morphism of a,b; :: thesis: ( f in <^a9,b9^> iff P2[a,b,f] )
thus ( f in <^a9,b9^> iff P2[a,b,f] ) by A30, A53, A54, A55; :: thesis: verum