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 CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C holds
( 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 & i = the Id of C | O )
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 CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C holds
( 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 & i = the Id of C | O )
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 CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C holds
( 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 & i = the Id of C | O )
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 CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C holds
( 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 & i = the Id of C | O )
let p be PartFunc of [:M,M:],M; :: thesis: for i being Function of O,M st CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C holds
( 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 & i = the Id of C | O )
let i be Function of O,M; :: thesis: ( CatStr(# O,M,d,c,p,i #) is_full_subcategory_of C implies ( 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 & i = the Id of C | O ) )
set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
set B = CatStr(# O,M,d,c,p,i #);
assume that
A1: CatStr(# O,M,d,c,p,i #) is Subcategory of C and
A2: 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) ; :: according to CAT_2:def 6 :: 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 & i = the Id of C | O )
A3: for f being Morphism of CatStr(# O,M,d,c,p,i #) holds
( d . f = the Source of C . f & c . f = the Target of C . f )

proof

let f be Morphism of CatStr(# O,M,d,c,p,i #); :: thesis: ( d . f = the Source of C . f & c . f = the Target of C . f )
reconsider f9 = f as Morphism of C by A1, Th14;
( dom f = dom f9 & cod f = cod f9 ) by A1, Th15;
hence ( d . f = the Source of C . f & c . f = the Target of C . f ) ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( x in M implies x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) & ( x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies x in M ) )
thus ( x in M implies x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) :: thesis: ( x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } implies x in M )

proof

assume x in M ; :: thesis: x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
then reconsider f = x as Morphism of CatStr(# O,M,d,c,p,i #) ;
reconsider f9 = f as Morphism of C by A1, Th14;
set a9 = dom f9;
set b9 = cod f9;
( the Source of CatStr(# O,M,d,c,p,i #) . f = the Source of C . f9 & the Target of CatStr(# O,M,d,c,p,i #) . f = the Target of C . f9 ) by A3;
then ( f in Hom ((dom f9),(cod f9)) & Hom ((dom f9),(cod f9)) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ) ;
hence x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4; :: thesis: verum

end;

assume x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ; :: thesis: x in M
then consider X being set such that
A4: x in X and
A5: X in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:def 4;
consider a9, b9 being Object of C such that
A6: X = Hom (a9,b9) and
A7: ( a9 in O & b9 in O ) by A5;
reconsider a = a9, b = b9 as Object of CatStr(# O,M,d,c,p,i #) by A7;
Hom (a,b) = Hom (a9,b9) by A2;
hence x in M by A4, A6; :: thesis: verum

end;

hence A8: M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by TARSKI:1; :: thesis: ( d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M & i = the Id of C | O )
then reconsider d9 = the Source of C | M, c9 = the Target of C | M as Function of M,O by Th29;
set p9 = the Comp of C || M;

now

let f be Element of M; :: thesis: d . f = d9 . f
d . f = the Source of C . f by A3;
hence d . f = d9 . f by FUNCT_1:49; :: thesis: verum

end;

hence d = the Source of C | M by FUNCT_2:63; :: thesis: ( c = the Target of C | M & p = the Comp of C || M & i = the Id of C | O )

now

let f be Element of M; :: thesis: c . f = c9 . f
c . f = the Target of C . f by A3;
hence c . f = c9 . f by FUNCT_1:49; :: thesis: verum

end;

hence c = the Target of C | M by FUNCT_2:63; :: thesis: ( p = the Comp of C || M & i = the Id of C | O )

now

A9: dom p c= [:M,M:] by RELAT_1:def 18;
A10: dom ( the Comp of C || M) = (dom the Comp of C) /\ [:M,M:] by RELAT_1:61;
the Comp of CatStr(# O,M,d,c,p,i #) c= the Comp of C by A1, Def4;
then dom p c= dom the Comp of C by GRFUNC_1:2;
then A11: dom p c= dom ( the Comp of C || M) by A9, A10, XBOOLE_1:19;
dom ( the Comp of C || M) c= dom p

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ( the Comp of C || M) or x in dom p )
assume A12: x in dom ( the Comp of C || M) ; :: thesis: x in dom p
then x in [:M,M:] by A10, XBOOLE_0:def 4;
then consider g, f being Element of M such that
A13: x = [g,f] by DOMAIN_1:1;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p,i #) ;
reconsider f9 = f, g9 = g as Morphism of C by A1, Th14;
[g,f] in dom the Comp of C by A10, A12, A13, XBOOLE_0:def 4;
then A14: dom g9 = cod f9 by CAT_1:15;
( cod f = cod f9 & dom g = dom g9 ) by A1, Th15;
hence x in dom p by A1, A13, A14, CAT_1:15; :: thesis: verum

end;

hence dom p = dom ( the Comp of C || M) by A11, XBOOLE_0:def 10; :: thesis: for x being set st x in dom p holds
p . x = ( the Comp of C || M) . x
let x be set ; :: thesis: ( x in dom p implies p . x = ( the Comp of C || M) . x )
assume A15: x in dom p ; :: thesis: p . x = ( the Comp of C || M) . x
then consider g, f being Element of M such that
A16: x = [g,f] by A9, DOMAIN_1:1;
reconsider f = f, g = g as Morphism of CatStr(# O,M,d,c,p,i #) ;
A17: dom g = cod f by A1, A15, A16, CAT_1:15;
reconsider f9 = f, g9 = g as Morphism of C by A1, Th14;
A18: ( cod f = cod f9 & dom g = dom g9 ) by A1, Th15;
p . x = p . (g,f) by A16;
hence p . x = g * f by A1, A17, CAT_1:16
.= g9 * f9 by A1, A17, Th17
.= the Comp of C . (g9,f9) by A18, A17, CAT_1:16
.= ( the Comp of C || M) . x by A11, A15, A16, FUNCT_1:47 ;
:: thesis: verum

end;

hence p = the Comp of C || M by FUNCT_1:2; :: thesis: i = the Id of C | O
reconsider i9 = the Id of C | O as Function of O,M by A8, Th29;

now

let a be Element of O; :: thesis: i . a = i9 . a

now

reconsider b = a as Object of CatStr(# O,M,d,c,p,i #) ;
reconsider a9 = a as Object of C ;
id b = id a9 by A1, Def4;
hence i . a = the Id of C . a ; :: thesis: ( a in O & a in dom the Id of C )
thus a in O ; :: thesis: a in dom the Id of C
a in the carrier of C ;
hence a in dom the Id of C by FUNCT_2:def 1; :: thesis: verum

end;

hence i . a = i9 . a by FUNCT_1:49; :: thesis: verum

end;

hence i = the Id of C | O by FUNCT_2:63; :: thesis: verum