let C be Category; 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 st CatStr(# O,M,d,c,p #) 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 )
let O be 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 st CatStr(# O,M,d,c,p #) 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 )
let M be non empty set ; for d, c being Function of M,O
for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) 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 )
let d, c be Function of M,O; for p being PartFunc of [:M,M:],M st CatStr(# O,M,d,c,p #) 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 )
let p be PartFunc of [:M,M:],M; ( CatStr(# O,M,d,c,p #) 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 ) )
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 #);
assume A1:
CatStr(# O,M,d,c,p #) is full Subcategory of C
; ( 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 )
A2:
for f being Morphism of CatStr(# O,M,d,c,p #) holds
( d . f = the Source of C . f & c . f = the Target of C . f )
now for x being object holds
( ( 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 ) )let x be
object ;
( ( 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 ) } )
( 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
;
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 #) ;
reconsider f9 =
f as
Morphism of
C by A1, Th4;
set a9 =
dom f9;
set b9 =
cod f9;
( the
Source of
CatStr(#
O,
M,
d,
c,
p #)
. f = the
Source of
C . f9 & the
Target of
CatStr(#
O,
M,
d,
c,
p #)
. f = the
Target of
C . f9 )
by A2;
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;
verum
end; assume
x in union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
;
x in Mthen consider X being
set such that A3:
x in X
and A4:
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 A5:
X = Hom (
a9,
b9)
and A6:
(
a9 in O &
b9 in O )
by A4;
reconsider a =
a9,
b =
b9 as
Object of
CatStr(#
O,
M,
d,
c,
p #)
by A6;
Hom (
a,
b)
= Hom (
a9,
b9)
by A1, Def6;
hence
x in M
by A3, A5;
verum end;
hence
M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
by TARSKI:2; ( d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )
then reconsider d9 = the Source of C | M, c9 = the Target of C | M as Function of M,O by Th16;
set p9 = the Comp of C || M;
hence
d = the Source of C | M
by FUNCT_2:63; ( c = the Target of C | M & p = the Comp of C || M )
hence
c = the Target of C | M
by FUNCT_2:63; p = the Comp of C || M
now ( dom p = dom ( the Comp of C || M) & ( for x being object st x in dom p holds
p . x = ( the Comp of C || M) . x ) )A7:
dom p c= [:M,M:]
by RELAT_1:def 18;
A8:
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 #)
c= the
Comp of
C
by A1, Def4;
then
dom p c= dom the
Comp of
C
by GRFUNC_1:2;
then A9:
dom p c= dom ( the Comp of C || M)
by A7, A8, XBOOLE_1:19;
dom ( the Comp of C || M) c= dom p
proof
let x be
object ;
TARSKI:def 3 ( not x in dom ( the Comp of C || M) or x in dom p )
assume A10:
x in dom ( the Comp of C || M)
;
x in dom p
then
x in [:M,M:]
by A8, XBOOLE_0:def 4;
then consider g,
f being
Element of
M such that A11:
x = [g,f]
by DOMAIN_1:1;
reconsider f =
f,
g =
g as
Morphism of
CatStr(#
O,
M,
d,
c,
p #) ;
reconsider f9 =
f,
g9 =
g as
Morphism of
C by A1, Th4;
[g,f] in dom the
Comp of
C
by A8, A10, A11, XBOOLE_0:def 4;
then A12:
dom g9 = cod f9
by CAT_1:15;
(
cod f = cod f9 &
dom g = dom g9 )
by A1, Th5;
hence
x in dom p
by A1, A11, A12, CAT_1:15;
verum
end; hence
dom p = dom ( the Comp of C || M)
by A9, XBOOLE_0:def 10;
for x being object st x in dom p holds
p . x = ( the Comp of C || M) . xlet x be
object ;
( x in dom p implies p . x = ( the Comp of C || M) . x )assume A13:
x in dom p
;
p . x = ( the Comp of C || M) . xthen consider g,
f being
Element of
M such that A14:
x = [g,f]
by A7, DOMAIN_1:1;
reconsider f =
f,
g =
g as
Morphism of
CatStr(#
O,
M,
d,
c,
p #) ;
A15:
dom g = cod f
by A1, A13, A14, CAT_1:15;
reconsider f9 =
f,
g9 =
g as
Morphism of
C by A1, Th4;
A16:
(
cod f = cod f9 &
dom g = dom g9 )
by A1, Th5;
p . x = p . (
g,
f)
by A14;
hence p . x =
g (*) f
by A1, A15, CAT_1:16
.=
g9 (*) f9
by A1, A15, Th7
.=
the
Comp of
C . (
g9,
f9)
by A16, A1, A13, A14, CAT_1:15, CAT_1:16
.=
( the Comp of C || M) . x
by A9, A13, A14, FUNCT_1:47
;
verum end;
hence
p = the Comp of C || M
by FUNCT_1:2; verum