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:49;
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:61;
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 5; :: thesis:

end;

assume d . g = c . f ; :: thesis:
then [g,f] in dom the Comp of C by A10, A11, CAT_1:def 5;
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:61; :: 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:47; :: 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:4;
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:49;
c . g = the Target of C . g by A3, FUNCT_1:49;
then A18: the Target of C . h = c . g by A15, A14, A16, A17, CAT_1:def 5;
d . f = the Source of C . f by A2, FUNCT_1:49;
then the Source of C . h = d . f by A15, A14, A16, A17, CAT_1:def 5;
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:49;
then A22: b = cod f9 by A21, CAT_1:1;
dom f = dom f9 by A2, FUNCT_1:49;
then a = dom f9 by A21, CAT_1:1;
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:49;
then A24: cod f = b9 by A23, CAT_1:1;
dom f = dom f9 by A2, FUNCT_1:49;
then dom f = a9 by A23, CAT_1:1;
hence x in Hom (a,b) by A20, A24; :: thesis:

end;

hence Hom (a,b) = Hom (a9,b9) by TARSKI:1; :: 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:49;
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:49
.= 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 5
.= d . f by A2, FUNCT_1:49 ;
:: thesis:
thus c . (p . (g,f)) = the Target of C . (p . [g,f]) by A3, A29, FUNCT_1:49
.= 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 5
.= c . g by A3, FUNCT_1:49 ; :: 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:49;
A34: c . f = the Target of C . f by A3, FUNCT_1:49;
A35: ( f is Morphism of C & d . h = the Source of C . h ) by A2, A6, FUNCT_1:49;
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 5
.= 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:49;
( d . (i . b) = the Source of C . (i . b) & c . (i . b) = the Target of C . (i . b) ) by A2, A3, FUNCT_1:49;
hence A38: ( d . (i . b) = b & c . (i . b) = b ) by A37, CAT_1:def 5; :: 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:49;
thus p . ((i . b),f) = the Comp of C . ((i . b),f) by A12, A38, A39
.= f by A37, A39, A40, CAT_1:def 5 ; :: 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:49;
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 5 ;
:: thesis:

end;

then reconsider B = CatStr(# O,M,d,c,p,i #) as Category by CAT_1:def 5;
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:49;
( ( 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:59;
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: