let C be Category; :: thesis: for O being non empty Subset of the carrier of C
for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category

let O be non empty Subset of the carrier of C; :: thesis: for M being non empty set
for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category

let M be non empty set ; :: thesis: for d, c being Function of M,O
for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category

let d, c be Function of M,O; :: thesis: for p being PartFunc of [:M,M:],M
for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category

let p be PartFunc of [:M,M:],M; :: thesis: for i being Function of O,M st M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M holds
CatStr(# O,M,d,c,p #) is Category

let i be Function of O,M; :: thesis: ( M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } & d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M implies CatStr(# O,M,d,c,p #) is Category )
set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
assume that
A1: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } and
A2: d = the Source of C | M and
A3: c = the Target of C | M and
A4: p = the Comp of C || M ; :: thesis: CatStr(# O,M,d,c,p #) is Category
set B = CatStr(# O,M,d,c,p #);
A5: now :: thesis: for f being Morphism of CatStr(# O,M,d,c,p #) holds f is Morphism of C
let f be Morphism of CatStr(# O,M,d,c,p #); :: thesis: f is Morphism of C
consider X being set such that
A6: f in X and
A7: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by ;
ex a, b being Object of C st
( X = Hom (a,b) & a in O & b in O ) by A7;
hence f is Morphism of C by A6; :: thesis: verum
end;
A8: for f, g being Morphism of CatStr(# O,M,d,c,p #) holds
( [g,f] in dom p iff d . g = c . f )
proof
let f, g be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( [g,f] in dom p iff d . g = c . f )
reconsider gg = g, ff = f as Morphism of C by A5;
A9: ( d . g = dom gg & c . f = cod ff ) by ;
thus ( [g,f] in dom p implies d . g = c . f ) :: thesis: ( d . g = c . f implies [g,f] in dom p )
proof
assume [g,f] in dom p ; :: thesis: d . g = c . f
then [g,f] in (dom the Comp of C) /\ [:M,M:] by ;
then [gg,ff] in dom the Comp of C by XBOOLE_0:def 4;
hence d . g = c . f by ; :: thesis: verum
end;
assume d . g = c . f ; :: thesis: [g,f] in dom p
then [g,f] in dom the Comp of C by ;
then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4;
hence [g,f] in dom p by ; :: thesis: verum
end;
A10: CatStr(# O,M,d,c,p #) is Category-like by A8;
A11: CatStr(# O,M,d,c,p #) is transitive
proof
thus for f, g being Morphism of CatStr(# O,M,d,c,p #) st dom g = cod f holds
( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) :: according to CAT_1:def 7 :: thesis: verum
proof
let f, g be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( dom g = cod f implies ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
reconsider ff = f, gg = g as Morphism of C by A5;
A12: ( d . g = dom gg & c . f = cod ff ) by ;
assume A13: dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
A14: [g,f] in dom the Comp of CatStr(# O,M,d,c,p #) by ;
A15: p . (g,f) = g (*) f by ;
A16: dom p c= dom the Comp of C by ;
A17: p . [g,f] = the Comp of C . (g,f) by
.= gg (*) ff by ;
thus dom (g (*) f) = dom (gg (*) ff) by
.= dom ff by
.= dom f by ; :: thesis: cod (g (*) f) = cod g
thus cod (g (*) f) = cod (gg (*) ff) by
.= cod gg by
.= cod g by ; :: thesis: verum
end;
end;
A18: CatStr(# O,M,d,c,p #) is associative
proof
thus for f, g, h being Morphism of CatStr(# O,M,d,c,p #) st dom h = cod g & dom g = cod f holds
h (*) (g (*) f) = (h (*) g) (*) f :: according to CAT_1:def 8 :: thesis: verum
proof
let f, g, h be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( dom h = cod g & dom g = cod f implies h (*) (g (*) f) = (h (*) g) (*) f )
reconsider ff = f, gg = g, hh = h as Morphism of C by A5;
assume that
A19: dom h = cod g and
A20: dom g = cod f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
A21: h (*) g = the Comp of CatStr(# O,M,d,c,p #) . (h,g) by ;
A22: g (*) f = the Comp of CatStr(# O,M,d,c,p #) . (g,f) by ;
A23: dom (h (*) g) = dom g by ;
A24: ( c . g = cod gg & d . g = dom gg ) by ;
A25: c . f = cod ff by ;
A26: ( f is Morphism of C & d . h = dom hh ) by ;
A27: dom gg = d . g by
.= cod ff by ;
then A28: gg (*) ff = the Comp of C . (gg,ff) by CAT_1:16;
A29: dom hh = d . h by
.= cod gg by ;
then A30: cod (gg (*) ff) = dom hh by ;
A31: hh (*) gg = the Comp of C . (hh,gg) by ;
A32: cod ff = dom (hh (*) gg) by ;
A33: cod (g (*) f) = cod g by ;
hence h (*) (g (*) f) = the Comp of CatStr(# O,M,d,c,p #) . (h,( the Comp of CatStr(# O,M,d,c,p #) . (g,f))) by
.= the Comp of C . [h,(p . [g,f])] by
.= the Comp of C . (hh,(gg (*) ff)) by
.= hh (*) (gg (*) ff) by
.= (hh (*) gg) (*) ff by
.= the Comp of C . (( the Comp of C . (hh,gg)),ff) by
.= the Comp of C . [(p . [h,g]),f] by
.= the Comp of CatStr(# O,M,d,c,p #) . (( the Comp of CatStr(# O,M,d,c,p #) . (h,g)),f) by
.= (h (*) g) (*) f by ;
:: thesis: verum
end;
end;
A34: CatStr(# O,M,d,c,p #) is reflexive
proof
let b be Object of CatStr(# O,M,d,c,p #); :: according to CAT_1:def 9 :: thesis: not Hom (b,b) = {}
b in O ;
then reconsider bb = b as Object of C ;
A35: Hom (bb,bb) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
id bb in Hom (bb,bb) by CAT_1:27;
then reconsider ii = id bb as Morphism of CatStr(# O,M,d,c,p #) by ;
A36: dom ii = dom (id bb) by
.= bb ;
cod ii = cod (id bb) by
.= bb ;
then ii in Hom (b,b) by A36;
hence Hom (b,b) <> {} ; :: thesis: verum
end;
CatStr(# O,M,d,c,p #) is with_identities
proof
let a be Element of CatStr(# O,M,d,c,p #); :: according to CAT_1:def 10 :: thesis: ex b1 being Morphism of a,a st
for b2 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b2) = {} or for b3 being Morphism of a,b2 holds b3 (*) b1 = b3 ) & ( Hom (b2,a) = {} or for b3 being Morphism of b2,a holds b1 (*) b3 = b3 ) )

a in O ;
then reconsider aa = a as Object of C ;
A37: Hom (aa,aa) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
id aa in Hom (aa,aa) by CAT_1:27;
then reconsider ii = id aa as Morphism of CatStr(# O,M,d,c,p #) by ;
A38: dom ii = dom (id aa) by
.= aa ;
A39: cod ii = cod (id aa) by
.= aa ;
then reconsider ii = ii as Morphism of a,a by ;
take ii ; :: thesis: for b1 being Element of the carrier of CatStr(# O,M,d,c,p #) holds
( ( Hom (a,b1) = {} or for b2 being Morphism of a,b1 holds b2 (*) ii = b2 ) & ( Hom (b1,a) = {} or for b2 being Morphism of b1,a holds ii (*) b2 = b2 ) )

let b be Element of CatStr(# O,M,d,c,p #); :: thesis: ( ( Hom (a,b) = {} or for b1 being Morphism of a,b holds b1 (*) ii = b1 ) & ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 ) )
b in O ;
then reconsider bb = b as Object of C ;
thus ( Hom (a,b) <> {} implies for g being Morphism of a,b holds g (*) ii = g ) :: thesis: ( Hom (b,a) = {} or for b1 being Morphism of b,a holds ii (*) b1 = b1 )
proof
assume A40: Hom (a,b) <> {} ; :: thesis: for g being Morphism of a,b holds g (*) ii = g
let g be Morphism of a,b; :: thesis: g (*) ii = g
reconsider gg = g as Morphism of C by A5;
A41: dom gg = dom g by
.= aa by ;
A42: cod (id aa) = aa ;
cod gg = cod g by
.= bb by ;
then reconsider gg = gg as Morphism of aa,bb by ;
A43: dom g = a by ;
hence g (*) ii = p . (g,ii) by
.= the Comp of C . (gg,(id aa)) by
.= gg (*) (id aa) by
.= g by ;
:: thesis: verum
end;
thus ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) :: thesis: verum
proof
assume A44: Hom (b,a) <> {} ; :: thesis: for f being Morphism of b,a holds ii (*) f = f
let g be Morphism of b,a; :: thesis: ii (*) g = g
reconsider gg = g as Morphism of C by A5;
A45: cod gg = cod g by
.= aa by ;
A46: dom (id aa) = aa ;
dom gg = dom g by
.= bb by ;
then reconsider gg = gg as Morphism of bb,aa by ;
A47: cod g = a by ;
hence ii (*) g = p . (ii,g) by
.= the Comp of C . ((id aa),gg) by
.= (id aa) (*) gg by
.= g by ;
:: thesis: verum
end;
end;
hence CatStr(# O,M,d,c,p #) is Category by A10, A11, A18, A34; :: thesis: verum