let A be Category; :: thesis:
let O be non empty Subset of the carrier of A; :: thesis:
let M be non empty Subset of the carrier' of A; :: thesis:
assume A1: for o being Element of A st o in O holds
id o in M ; :: thesis:
let DOM, COD be Function of M,O; :: thesis:
assume that
A2: DOM = the Source of A | M and
A3: COD = the Target of A | M ; :: thesis:
let COMP be PartFunc of [:M,M:],M; :: thesis:
assume A4: COMP = the Comp of A || M ; :: thesis:
set C = CatStr(# O,M,DOM,COD,COMP #);

let f be Morphism of A; :: thesis:
let g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: thesis:
assume A6: f = g ; :: thesis:
dom the Source of CatStr(# O,M,DOM,COD,COMP #) = the carrier' of CatStr(# O,M,DOM,COD,COMP #) by FUNCT_2:def 1;
hence dom f = dom g by A2, A6, FUNCT_1:47; :: thesis:
dom the Target of CatStr(# O,M,DOM,COD,COMP #) = the carrier' of CatStr(# O,M,DOM,COD,COMP #) by FUNCT_2:def 1;
hence cod f = cod g by A3, A6, FUNCT_1:47; :: thesis:

end;

A7: dom the Comp of CatStr(# O,M,DOM,COD,COMP #) = (dom the Comp of A) /\ [: the carrier' of CatStr(# O,M,DOM,COD,COMP #), the carrier' of CatStr(# O,M,DOM,COD,COMP #):] by A4, RELAT_1:61;

A8: now :: thesis:

let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: thesis:
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;
assume dom g = cod f ; :: thesis:
then dom g9 = cod f by A5
.= cod f9 by A5 ;
then A9: [g9,f9] in dom the Comp of A by CAT_1:def 6;
[g,f] in [: the carrier' of CatStr(# O,M,DOM,COD,COMP #), the carrier' of CatStr(# O,M,DOM,COD,COMP #):] by ZFMISC_1:87;
hence [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A7, A9, XBOOLE_0:def 4; :: thesis:

end;

A10: dom the Comp of CatStr(# O,M,DOM,COD,COMP #) c= dom the Comp of A by A4, RELAT_1:60;
A11: CatStr(# O,M,DOM,COD,COMP #) is Category-like

proof

let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def 6 :: thesis:
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;
thus ( [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) implies dom g = cod f ) :: thesis:

proof

assume A12: [g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) ; :: thesis:
thus dom g = dom g9 by A5
.= cod f9 by A10, A12, CAT_1:def 6
.= cod f by A5 ; :: thesis:

end;

thus ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# O,M,DOM,COD,COMP #) ) by A8; :: thesis:

end;

A13: CatStr(# O,M,DOM,COD,COMP #) is transitive

proof

let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def 7 :: thesis:
reconsider g9 = g, f9 = f as Morphism of A by TARSKI:def 3;
assume A14: dom g = cod f ; :: thesis:
[g,f] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A14, A11;
then A15: the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = g (*) f by CAT_1:def 1;
A16: dom g9 = cod f by A5, A14
.= cod f9 by A5 ;
then [g9,f9] in dom the Comp of A by CAT_1:def 6;
then A17: the Comp of A . (g9,f9) = g9 (*) f9 by CAT_1:def 1;
A18: the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = the Comp of A . (g9,f9) by A4, A8, A14, FUNCT_1:47;
thus dom (g (*) f) = dom (g9 (*) f9) by A5, A18, A15, A17
.= dom f9 by A16, CAT_1:def 7
.= dom f by A5 ; :: thesis:
thus cod (g (*) f) = cod (g9 (*) f9) by A5, A18, A15, A17
.= cod g9 by A16, CAT_1:def 7
.= cod g by A5 ; :: thesis:

end;

A19: for f, g being Morphism of CatStr(# O,M,DOM,COD,COMP #) st cod g = dom f holds
for ff, gg being Morphism of A st ff = f & gg = g holds
f (*) g = ff (*) gg

proof

let f, g be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: thesis:
assume A20: cod g = dom f ; :: thesis:
let ff, gg be Morphism of A; :: thesis:
assume A21: ( ff = f & gg = g ) ; :: thesis:
A22: cod gg = dom f by A20, A5, A21
.= dom ff by A5, A21 ;
[f,g] in dom the Comp of CatStr(# O,M,DOM,COD,COMP #) by A20, A11;
hence f (*) g = the Comp of CatStr(# O,M,DOM,COD,COMP #) . (f,g) by CAT_1:def 1
.= the Comp of A . (ff,gg) by A21, A4, A8, A20, FUNCT_1:47
.= ff (*) gg by A22, CAT_1:16 ;
:: thesis:

end;

A23: CatStr(# O,M,DOM,COD,COMP #) is associative

proof

let f, g, h be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def 8 :: thesis:
reconsider g9 = g, f9 = f, h9 = h as Morphism of A by TARSKI:def 3;
assume that
A24: dom h = cod g and
A25: dom g = cod f ; :: thesis:
reconsider gf = the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f), hg = the Comp of CatStr(# O,M,DOM,COD,COMP #) . [h,g] as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A8, A24, A25, PARTFUN1:4;
A26: dom h9 = cod g by A5, A24
.= cod g9 by A5 ;
then A27: [h9,g9] in dom the Comp of A by CAT_1:def 6;
A28: dom g9 = cod f by A5, A25
.= cod f9 by A5 ;
then A29: [g9,f9] in dom the Comp of A by CAT_1:def 6;
reconsider gf9 = g9 (*) f9, hg9 = h9 (*) g9 as Morphism of A ;
the Comp of CatStr(# O,M,DOM,COD,COMP #) . (h,g) = the Comp of A . (h9,g9) by A4, A8, A24, FUNCT_1:47;
then A30: hg = h9 (*) g9 by A27, CAT_1:def 1;
then A31: dom hg = dom hg9 by A5
.= dom g9 by A26, CAT_1:def 7
.= cod f by A5, A25 ;
the Comp of CatStr(# O,M,DOM,COD,COMP #) . (g,f) = the Comp of A . (g9,f9) by A4, A8, A25, FUNCT_1:47;
then A32: gf = gf9 by A29, CAT_1:def 1;
A33: dom h = cod g9 by A5, A24
.= cod gf9 by A28, CAT_1:def 7
.= cod gf by A5, A32 ;
A34: h (*) g = h9 (*) g9 by A19, A24;
g (*) f = g9 (*) f9 by A19, A25;
hence h (*) (g (*) f) = h9 (*) (g9 (*) f9) by A19, A33, A32
.= (h9 (*) g9) (*) f9 by A26, A28, CAT_1:def 8
.= (h (*) g) (*) f by A19, A34, A30, A31 ;
:: thesis:

end;

A35: CatStr(# O,M,DOM,COD,COMP #) is reflexive

proof

let b be Object of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def 9 :: thesis:
reconsider b9 = b as Object of A by TARSKI:def 3;
reconsider ii = id b9 as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A1;
A36: cod ii = cod (id b9) by A5
.= b ;
dom ii = dom (id b9) by A5
.= b ;
then ii in Hom (b,b) by A36;
hence Hom (b,b) <> {} ; :: thesis:

end;

A37: for a being Object of CatStr(# O,M,DOM,COD,COMP #)
for aa being Element of A st a = aa holds
for m being Morphism of CatStr(# O,M,DOM,COD,COMP #) st m = id aa holds
for b being Object of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )

proof

let a be Object of CatStr(# O,M,DOM,COD,COMP #); :: thesis:
let aa be Element of A; :: thesis:
assume A38: a = aa ; :: thesis:
let m be Morphism of CatStr(# O,M,DOM,COD,COMP #); :: thesis:
assume A39: m = id aa ; :: thesis:
let b be Object of CatStr(# O,M,DOM,COD,COMP #); :: thesis:
reconsider bb = b as Object of A by TARSKI:def 3;
thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) :: thesis:

proof

assume A40: Hom (a,b) <> {} ; :: thesis:
let f be Morphism of a,b; :: thesis:
reconsider ff = f as Morphism of A by TARSKI:def 3;
dom f = a by A40, CAT_1:5;
then A41: dom ff = aa by A38, A5;
dom f = cod (id aa) by A38, A40, CAT_1:5
.= cod m by A39, A5 ;
hence f (*) m = ff (*) (id aa) by A19, A39
.= f by A41, CAT_1:22 ;
:: thesis:

end;

thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) :: thesis:

proof

assume A42: Hom (b,a) <> {} ; :: thesis:
let f be Morphism of b,a; :: thesis:
reconsider ff = f as Morphism of A by TARSKI:def 3;
cod f = a by A42, CAT_1:5;
then A43: cod ff = aa by A38, A5;
dom f = b by A42, CAT_1:5;
then dom ff = bb by A5;
then A44: ff in Hom (bb,aa) by A43;
then reconsider ff = ff as Morphism of bb,aa by CAT_1:def 5;
A45: Hom (aa,aa) <> {} ;
cod f = dom (id aa) by A38, A42, CAT_1:5
.= dom m by A39, A5 ;
hence m (*) f = (id aa) (*) ff by A19, A39
.= (id aa) * ff by A44, A45, CAT_1:def 13
.= f by A44, CAT_1:28 ;
:: thesis:

end;

CatStr(# O,M,DOM,COD,COMP #) is with_identities

proof

let a be Element of CatStr(# O,M,DOM,COD,COMP #); :: according to CAT_1:def 10 :: thesis:
reconsider aa = a as Element of A by TARSKI:def 3;
reconsider m = id aa as Morphism of CatStr(# O,M,DOM,COD,COMP #) by A1;
A46: cod m = cod (id aa) by A5
.= a ;
dom m = dom (id aa) by A5
.= a ;
then m in Hom (a,a) by A46;
then reconsider m = m as Morphism of a,a by CAT_1:def 5;
take m ; :: thesis:
thus for b₁ being Element of the carrier of CatStr(# O,M,DOM,COD,COMP #) holds
( ( Hom (a,b₁) = {} or for b₂ being Morphism of a,b₁ holds b₂ (*) m = b₂ ) & ( Hom (b₁,a) = {} or for b₂ being Morphism of b₁,a holds m (*) b₂ = b₂ ) ) by A37; :: thesis:

end;

then reconsider C = CatStr(# O,M,DOM,COD,COMP #) as Category by A11, A13, A23, A35;
C is Subcategory of A

proof

thus the carrier of C c= the carrier of A ; :: according to CAT_2:def 4 :: thesis:
thus for a, b being Object of C
for a9, b9 being Object of A st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) :: thesis:

proof

let a, b be Object of C; :: thesis:
let a9, b9 be Object of A; :: thesis:
assume that
A47: a = a9 and
A48: b = b9 ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Hom (a,b) ; :: thesis:
then consider f being Morphism of C such that
A49: x = f and
A50: dom f = a and
A51: cod f = b ;
reconsider f9 = f as Morphism of A by TARSKI:def 3;
A52: cod f9 = b9 by A5, A48, A51;
dom f9 = a9 by A5, A47, A50;
hence x in Hom (a9,b9) by A49, A52; :: thesis:

end;

thus the Comp of C c= the Comp of A by A4, RELAT_1:59; :: thesis:
let a be Object of C; :: thesis:
let a9 be Object of A; :: thesis:
assume A53: a = a9 ; :: thesis:
reconsider m = id a9 as Morphism of C by A1, A53;
A54: cod m = cod (id a9) by A5
.= a by A53 ;
dom m = dom (id a9) by A5
.= a by A53 ;
then m in Hom (a,a) by A54;
then reconsider m = m as Morphism of a,a by CAT_1:def 5;
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) by A53, A37;
hence id a = id a9 by CAT_1:def 12; :: thesis:

end;

hence CatStr(# O,M,DOM,COD,COMP #) is Subcategory of A ; :: thesis: