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 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: 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 )

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 )

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;

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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: 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 )

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 )

proof

let f be Morphism of CatStr(# O,M,d,c,p #); :: thesis: ( d . f = the Source of C . f & c . f = the Target of C . f )

reconsider f9 = f as Morphism of C by A1, Th4;

( dom f = dom f9 & cod f = cod f9 ) by A1, Th5;

hence ( d . f = the Source of C . f & c . f = the Target of C . f ) ; :: thesis: verum

end;reconsider f9 = f as Morphism of C by A1, Th4;

( dom f = dom f9 & cod f = cod f9 ) by A1, Th5;

hence ( d . f = the Source of C . f & c . f = the Target of C . f ) ; :: thesis: verum

now :: thesis: 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 ) )

hence
M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
by TARSKI:2; :: thesis: ( d = the Source of C | M & c = the Target of C | M & p = the Comp of C || M )( ( 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 ; :: 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 )

then 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; :: thesis: verum

end;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 union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) }
; :: thesis: x in M
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 #) ;

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; :: thesis: verum

end;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; :: thesis: verum

then 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; :: thesis: verum

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;

now :: thesis: for f being Element of M holds d . f = d9 . f

hence
d = the Source of C | M
by FUNCT_2:63; :: thesis: ( c = the Target of C | M & p = the Comp of C || M )let f be Element of M; :: thesis: d . f = d9 . f

d . f = the Source of C . f by A2;

hence d . f = d9 . f by FUNCT_1:49; :: thesis: verum

end;d . f = the Source of C . f by A2;

hence d . f = d9 . f by FUNCT_1:49; :: thesis: verum

now :: thesis: for f being Element of M holds c . f = c9 . f

hence
c = the Target of C | M
by FUNCT_2:63; :: thesis: p = the Comp of C || Mlet f be Element of M; :: thesis: c . f = c9 . f

c . f = the Target of C . f by A2;

hence c . f = c9 . f by FUNCT_1:49; :: thesis: verum

end;c . f = the Target of C . f by A2;

hence c . f = c9 . f by FUNCT_1:49; :: thesis: verum

now :: thesis: ( 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 ) )

hence
p = the Comp of C || M
by FUNCT_1:2; :: thesis: verump . 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

p . x = ( the Comp of C || M) . x

let x be object ; :: thesis: ( x in dom p implies p . x = ( the Comp of C || M) . x )

assume A13: x in dom p ; :: thesis: p . x = ( the Comp of C || M) . x

then 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 ;

:: thesis: verum

end;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

hence
dom p = dom ( the Comp of C || M)
by A9, XBOOLE_0:def 10; :: thesis: for x being object st x in dom p holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ( the Comp of C || M) or x in dom p )

assume A10: x in dom ( the Comp of C || M) ; :: thesis: 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; :: thesis: verum

end;assume A10: x in dom ( the Comp of C || M) ; :: thesis: 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; :: thesis: verum

p . x = ( the Comp of C || M) . x

let x be object ; :: thesis: ( x in dom p implies p . x = ( the Comp of C || M) . x )

assume A13: x in dom p ; :: thesis: p . x = ( the Comp of C || M) . x

then 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 ;

:: thesis: verum