let C be Category; :: thesis:
let O be non empty Subset of the carrier of C; :: thesis:
let M be non empty set ; :: thesis:
let d, c be Function of M,O; :: thesis:
let p be PartFunc of [:M,M:],M; :: thesis:
let i be Function of O,M; :: thesis:
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 and
A5: i = the Id of C | O ; :: thesis:
set B = CatStr(# O,M,d,c,p,i #);

A6: now

let f be Morphism of CatStr(# O,M,d,c,p,i #); :: thesis:
consider X being set such that
A7: f in X and
A8: X in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } by A1, TARSKI:def 4;
ex a, b being Object of C st
( X = Hom a,b & a in O & b in O ) by A8;
hence f is Morphism of C by A7; :: thesis:

end;

A9: for f, g being Element of M holds
( [g,f] in dom p iff d . g = c . f )

proof

let f, g be Element of M; :: thesis:
A10: ( g is Morphism of C & f is Morphism of C ) by A6;
A11: ( d . g = the Source of C . g & c . f = the Target of C . f ) by A2, A3, FUNCT_1:72;
thus ( [g,f] in dom p implies d . g = c . f ) :: thesis:

proof

assume [g,f] in dom p ; :: thesis:
then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:90;
then [g,f] in dom the Comp of C by XBOOLE_0:def 4;
hence d . g = c . f by A10, A11, CAT_1:def 8; :: thesis:

end;

assume d . g = c . f ; :: thesis:
then [g,f] in dom the Comp of C by A10, A11, CAT_1:def 8;
then [g,f] in (dom the Comp of C) /\ [:M,M:] by XBOOLE_0:def 4;
hence [g,f] in dom p by A4, RELAT_1:90; :: thesis:

end;

A12: for f, g being Element of M st d . g = c . f holds
p . [g,f] = the Comp of C . [g,f]

proof

let f, g be Element of M; :: thesis:
assume d . g = c . f ; :: thesis:
then [g,f] in dom p by A9;
hence p . [g,f] = the Comp of C . [g,f] by A4, FUNCT_1:70; :: thesis:

end;

A13: for f, g being Element of M st d . g = c . f holds
p . [g,f] is Element of M

proof

let f, g be Element of M; :: thesis:
A14: ( f is Morphism of C & g is Morphism of C ) by A6;
assume A15: d . g = c . f ; :: thesis:
then [g,f] in dom p by A9;
then p . [g,f] is Element of M by PARTFUN1:27;
then reconsider h = p . [g,f] as Morphism of C by A6;
A16: h = the Comp of C . g,f by A12, A15;
set a = dom h;
set b = cod h;
A17: ( d . g = the Source of C . g & c . f = the Target of C . f ) by A2, A3, FUNCT_1:72;
c . g = the Target of C . g by A3, FUNCT_1:72;
then A18: the Target of C . h = c . g by A15, A14, A16, A17, CAT_1:def 8;
d . f = the Source of C . f by A2, FUNCT_1:72;
then the Source of C . h = d . f by A15, A14, A16, A17, CAT_1:def 8;
then ( h in Hom (dom h),(cod h) & Hom (dom h),(cod h) in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } ) by A18;
hence p . [g,f] is Element of M by A1, TARSKI:def 4; :: thesis:

end;

A19: for a, b being Object of CatStr(# O,M,d,c,p,i #)
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom a,b = Hom a9,b9

proof

let a, b be Object of CatStr(# O,M,d,c,p,i #); :: thesis:
let a9, b9 be Object of C; :: thesis:
assume A20: ( a = a9 & b = b9 ) ; :: thesis:

now

let x be set ; :: thesis:
thus ( x in Hom a,b implies x in Hom a9,b9 ) :: thesis:

proof

assume A21: x in Hom a,b ; :: thesis:
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p,i #) ;
reconsider f9 = f as Morphism of C by A6;
cod f = cod f9 by A3, FUNCT_1:72;
then A22: b = cod f9 by A21, CAT_1:18;
dom f = dom f9 by A2, FUNCT_1:72;
then a = dom f9 by A21, CAT_1:18;
hence x in Hom a9,b9 by A20, A22; :: thesis:

end;

assume A23: x in Hom a9,b9 ; :: thesis:
then reconsider f9 = x as Morphism of C ;
Hom a9,b9 in { (Hom a,b) where a, b is Object of C : ( a in O & b in O ) } by A20;
then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p,i #) by A1, A23, TARSKI:def 4;
cod f = cod f9 by A3, FUNCT_1:72;
then A24: cod f = b9 by A23, CAT_1:18;
dom f = dom f9 by A2, FUNCT_1:72;
then dom f = a9 by A23, CAT_1:18;
hence x in Hom a,b by A20, A24; :: thesis:

end;

hence Hom a,b = Hom a9,b9 by TARSKI:2; :: thesis:

end;

thus CatStr(# O,M,d,c,p,i #) is Subcategory of C :: according to CAT_2:def 6 :: thesis:

proof

now

thus for f, g being Element of M holds
( [g,f] in dom p iff d . g = c . f ) by A9; :: thesis:
thus A25: for f, g being Element of M st d . g = c . f holds
( d . (p . g,f) = d . f & c . (p . g,f) = c . g ) :: thesis:

proof

let f, g be Element of M; :: thesis:
A26: ( g is Morphism of C & f is Morphism of C ) by A6;
A27: ( d . g = the Source of C . g & c . f = the Target of C . f ) by A2, A3, FUNCT_1:72;
assume A28: d . g = c . f ; :: thesis:
then A29: p . [g,f] is Element of M by A13;
hence d . (p . g,f) = the Source of C . (p . [g,f]) by A2, FUNCT_1:72
.= the Source of C . (the Comp of C . g,f) by A12, A28
.= the Source of C . f by A28, A26, A27, CAT_1:def 8
.= d . f by A2, FUNCT_1:72 ;
:: thesis:
thus c . (p . g,f) = the Target of C . (p . [g,f]) by A3, A29, FUNCT_1:72
.= the Target of C . (the Comp of C . g,f) by A12, A28
.= the Target of C . g by A28, A26, A27, CAT_1:def 8
.= c . g by A3, FUNCT_1:72 ; :: thesis:

end;

thus for f, g, h being Element of M st d . h = c . g & d . g = c . f holds
p . h,(p . g,f) = p . (p . h,g),f :: thesis:

proof

let f, g, h be Element of M; :: thesis:
assume that
A30: d . h = c . g and
A31: d . g = c . f ; :: thesis:
A32: ( d . (p . h,g) = d . g & p . h,g is Element of M ) by A13, A25, A30;
A33: ( c . g = the Target of C . g & d . g = the Source of C . g ) by A2, A3, FUNCT_1:72;
A34: c . f = the Target of C . f by A3, FUNCT_1:72;
A35: ( f is Morphism of C & d . h = the Source of C . h ) by A2, A6, FUNCT_1:72;
A36: ( h is Morphism of C & g is Morphism of C ) by A6;
( c . (p . g,f) = c . g & p . [g,f] is Element of M ) by A13, A25, A31;
hence p . h,(p . g,f) = the Comp of C . [h,(p . [g,f])] by A12, A30
.= the Comp of C . h,(the Comp of C . g,f) by A12, A31
.= the Comp of C . (the Comp of C . h,g),f by A30, A31, A36, A35, A33, A34, CAT_1:def 8
.= the Comp of C . [(p . [h,g]),f] by A12, A30
.= p . (p . h,g),f by A12, A31, A32 ;
:: thesis:

end;

let b be Element of O; :: thesis:
A37: i . b = the Id of C . b by A5, FUNCT_1:72;
( d . (i . b) = the Source of C . (i . b) & c . (i . b) = the Target of C . (i . b) ) by A2, A3, FUNCT_1:72;
hence A38: ( d . (i . b) = b & c . (i . b) = b ) by A37, CAT_1:def 8; :: thesis:
thus for f being Element of M st c . f = b holds
p . (i . b),f = f :: thesis:

proof

let f be Element of M; :: thesis:
assume A39: c . f = b ; :: thesis:
A40: ( f is Morphism of C & c . f = the Target of C . f ) by A3, A6, FUNCT_1:72;
thus p . (i . b),f = the Comp of C . (i . b),f by A12, A38, A39
.= f by A37, A39, A40, CAT_1:def 8 ; :: thesis:

end;

let g be Element of M; :: thesis:
A41: ( g is Morphism of C & d . g = the Source of C . g ) by A2, A6, FUNCT_1:72;
assume A42: d . g = b ; :: thesis:
hence p . g,(i . b) = the Comp of C . g,(i . b) by A12, A38
.= g by A37, A42, A41, CAT_1:def 8 ;
:: thesis:

end;

then reconsider B = CatStr(# O,M,d,c,p,i #) as Category by CAT_1:def 8;
A43: for a being Object of B
for a9 being Object of C st a = a9 holds
id a = id a9 by A5, FUNCT_1:72;
( ( for a, b being Object of B
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom a,b c= Hom a9,b9 ) & the Comp of B c= the Comp of C ) by A4, A19, RELAT_1:88;
hence CatStr(# O,M,d,c,p,i #) is Subcategory of C by A43, Def4; :: thesis:

end;

thus for a, b being Object of CatStr(# O,M,d,c,p,i #)
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom a,b = Hom a9,b9 by A19; :: thesis: