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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

let p be PartFunc of [:M,M:],M; :: thesis: for i being Function of O,M st 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

let i be Function of O,M; :: 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 implies CatStr(# O,M,d,c,p #) is Subcategory of C )

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 ; :: thesis: CatStr(# O,M,d,c,p #) is Subcategory of C

set B = CatStr(# O,M,d,c,p #);

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9)

A14: for a being Object of B

for a9 being Object of C st a = a9 holds

id a = id a9

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, A8, RELAT_1:59;

hence CatStr(# O,M,d,c,p #) is Subcategory of C by A14, Def4; :: thesis: verum

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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

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 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

let p be PartFunc of [:M,M:],M; :: thesis: for i being Function of O,M st 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 holds

CatStr(# O,M,d,c,p #) is Subcategory of C

let i be Function of O,M; :: 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 implies CatStr(# O,M,d,c,p #) is Subcategory of C )

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 ; :: thesis: CatStr(# O,M,d,c,p #) is Subcategory of C

set B = CatStr(# O,M,d,c,p #);

A5: now :: thesis: for f being Morphism of CatStr(# O,M,d,c,p #) holds f is Morphism of C

A8:
for a, b being Object of CatStr(# O,M,d,c,p #)let f be Morphism of CatStr(# O,M,d,c,p #); :: thesis: f is Morphism of C

consider X being set such that

A6: f in X and

A7: 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 A7;

hence f is Morphism of C by A6; :: thesis: verum

end;consider X being set such that

A6: f in X and

A7: 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 A7;

hence f is Morphism of C by A6; :: thesis: verum

for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9)

proof

reconsider B = CatStr(# O,M,d,c,p #) as Category by Lm1, A1, A2, A3, A4;
let a, b be Object of CatStr(# O,M,d,c,p #); :: thesis: for a9, b9 being Object of C st a = a9 & b = b9 holds

Hom (a,b) = Hom (a9,b9)

let a9, b9 be Object of C; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )

assume A9: ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) = Hom (a9,b9)

end;Hom (a,b) = Hom (a9,b9)

let a9, b9 be Object of C; :: thesis: ( a = a9 & b = b9 implies Hom (a,b) = Hom (a9,b9) )

assume A9: ( a = a9 & b = b9 ) ; :: thesis: Hom (a,b) = Hom (a9,b9)

now :: thesis: for x being object holds

( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )

hence
Hom (a,b) = Hom (a9,b9)
by TARSKI:2; :: thesis: verum( ( x in Hom (a,b) implies x in Hom (a9,b9) ) & ( x in Hom (a9,b9) implies x in Hom (a,b) ) )

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

thus ( x in Hom (a,b) implies x in Hom (a9,b9) ) :: thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )

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

then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p #) by A1, A12, TARSKI:def 4;

cod f = cod f9 by A3, FUNCT_1:49;

then A13: cod f = b9 by A12, CAT_1:1;

dom f = dom f9 by A2, FUNCT_1:49;

then dom f = a9 by A12, CAT_1:1;

hence x in Hom (a,b) by A9, A13; :: thesis: verum

end;thus ( x in Hom (a,b) implies x in Hom (a9,b9) ) :: thesis: ( x in Hom (a9,b9) implies x in Hom (a,b) )

proof

assume A12:
x in Hom (a9,b9)
; :: thesis: x in Hom (a,b)
assume A10:
x in Hom (a,b)
; :: thesis: x in Hom (a9,b9)

then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ;

reconsider f9 = f as Morphism of C by A5;

cod f = cod f9 by A3, FUNCT_1:49;

then A11: b = cod f9 by A10, CAT_1:1;

dom f = dom f9 by A2, FUNCT_1:49;

then a = dom f9 by A10, CAT_1:1;

hence x in Hom (a9,b9) by A9, A11; :: thesis: verum

end;then reconsider f = x as Morphism of CatStr(# O,M,d,c,p #) ;

reconsider f9 = f as Morphism of C by A5;

cod f = cod f9 by A3, FUNCT_1:49;

then A11: b = cod f9 by A10, CAT_1:1;

dom f = dom f9 by A2, FUNCT_1:49;

then a = dom f9 by A10, CAT_1:1;

hence x in Hom (a9,b9) by A9, A11; :: thesis: verum

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

then reconsider f = f9 as Morphism of CatStr(# O,M,d,c,p #) by A1, A12, TARSKI:def 4;

cod f = cod f9 by A3, FUNCT_1:49;

then A13: cod f = b9 by A12, CAT_1:1;

dom f = dom f9 by A2, FUNCT_1:49;

then dom f = a9 by A12, CAT_1:1;

hence x in Hom (a,b) by A9, A13; :: thesis: verum

A14: for a being Object of B

for a9 being Object of C st a = a9 holds

id a = id a9

proof

( ( for a, b being Object of B
let a be Object of B; :: thesis: for a9 being Object of C st a = a9 holds

id a = id a9

let a9 be Object of C; :: thesis: ( a = a9 implies id a = id a9 )

assume A15: a = a9 ; :: thesis: id a = id a9

A16: Hom (a9,a9) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A15;

A17: id a9 in Hom (a9,a9) by CAT_1:27;

then reconsider ii = id a9 as Morphism of B by A16, A1, TARSKI:def 4;

A18: dom ii = dom (id a9) by A2, FUNCT_1:49

.= a9 ;

A19: cod ii = cod (id a9) by A3, FUNCT_1:49

.= a9 ;

ii in Hom (a,a) by A17, A8, A15;

then reconsider ii = ii as Morphism of a,a by CAT_1:def 5;

A20: for f, g being Morphism of B holds

( [g,f] in dom p iff d . g = c . f )

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )

end;id a = id a9

let a9 be Object of C; :: thesis: ( a = a9 implies id a = id a9 )

assume A15: a = a9 ; :: thesis: id a = id a9

A16: Hom (a9,a9) in { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } by A15;

A17: id a9 in Hom (a9,a9) by CAT_1:27;

then reconsider ii = id a9 as Morphism of B by A16, A1, TARSKI:def 4;

A18: dom ii = dom (id a9) by A2, FUNCT_1:49

.= a9 ;

A19: cod ii = cod (id a9) by A3, FUNCT_1:49

.= a9 ;

ii in Hom (a,a) by A17, A8, A15;

then reconsider ii = ii as Morphism of a,a by CAT_1:def 5;

A20: for f, g being Morphism of B holds

( [g,f] in dom p iff d . g = c . f )

proof

for b being Object of B holds
let f, g be Morphism of B; :: thesis: ( [g,f] in dom p iff d . g = c . f )

reconsider gg = g, ff = f as Morphism of C by A5;

A21: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;

thus ( [g,f] in dom p implies d . g = c . f ) :: thesis: ( d . g = c . f implies [g,f] in dom p )

then [g,f] in dom the Comp of C by A21, CAT_1:def 6;

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

end;reconsider gg = g, ff = f as Morphism of C by A5;

A21: ( d . g = dom gg & c . f = cod ff ) by A2, A3, FUNCT_1:49;

thus ( [g,f] in dom p implies d . g = c . f ) :: thesis: ( d . g = c . f implies [g,f] in dom p )

proof

assume
d . g = c . f
; :: thesis: [g,f] in dom p
assume
[g,f] in dom p
; :: thesis: d . g = c . f

then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61;

then [gg,ff] in dom the Comp of C by XBOOLE_0:def 4;

hence d . g = c . f by A21, CAT_1:def 6; :: thesis: verum

end;then [g,f] in (dom the Comp of C) /\ [:M,M:] by A4, RELAT_1:61;

then [gg,ff] in dom the Comp of C by XBOOLE_0:def 4;

hence d . g = c . f by A21, CAT_1:def 6; :: thesis: verum

then [g,f] in dom the Comp of C by A21, CAT_1:def 6;

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

( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )

proof

hence
id a = id a9
by CAT_1:def 12; :: thesis: verum
let b be Object of B; :: thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )

b in O ;

then reconsider bb = b as Element of C ;

thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) :: thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )

let g be Morphism of b,a; :: thesis: ii (*) g = g

reconsider gg = g as Morphism of C by A5;

A27: cod gg = cod g by A3, FUNCT_1:49

.= a9 by A15, A26, CAT_1:5 ;

A28: dom (id a9) = a9 ;

dom gg = dom g by A2, FUNCT_1:49

.= bb by A26, CAT_1:5 ;

then reconsider gg = gg as Morphism of bb,a9 by A27, CAT_1:4;

A29: cod g = a by A26, CAT_1:5;

hence ii (*) g = p . (ii,g) by A18, A20, A15, CAT_1:def 1

.= the Comp of C . ((id a9),gg) by A18, A20, A15, A4, A29, FUNCT_1:47

.= (id a9) (*) gg by A27, A28, CAT_1:16

.= g by A27, CAT_1:21 ;

:: thesis: verum

end;b in O ;

then reconsider bb = b as Element of C ;

thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) :: thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )

proof

assume A26:
Hom (b,a) <> {}
; :: thesis: for f being Morphism of b,a holds ii (*) f = f
assume A22:
Hom (a,b) <> {}
; :: thesis: for f being Morphism of a,b holds f (*) ii = f

let g be Morphism of a,b; :: thesis: g (*) ii = g

reconsider gg = g as Morphism of C by A5;

A23: dom gg = dom g by A2, FUNCT_1:49

.= a9 by A15, A22, CAT_1:5 ;

A24: cod (id a9) = a9 ;

cod gg = cod g by A3, FUNCT_1:49

.= bb by A22, CAT_1:5 ;

then reconsider gg = gg as Morphism of a9,bb by A23, CAT_1:4;

A25: dom g = a by A22, CAT_1:5;

hence g (*) ii = p . (g,ii) by A19, A20, A15, CAT_1:def 1

.= the Comp of C . (gg,(id a9)) by A19, A20, A15, A4, A25, FUNCT_1:47

.= gg (*) (id a9) by A23, A24, CAT_1:16

.= g by A23, CAT_1:22 ;

:: thesis: verum

end;let g be Morphism of a,b; :: thesis: g (*) ii = g

reconsider gg = g as Morphism of C by A5;

A23: dom gg = dom g by A2, FUNCT_1:49

.= a9 by A15, A22, CAT_1:5 ;

A24: cod (id a9) = a9 ;

cod gg = cod g by A3, FUNCT_1:49

.= bb by A22, CAT_1:5 ;

then reconsider gg = gg as Morphism of a9,bb by A23, CAT_1:4;

A25: dom g = a by A22, CAT_1:5;

hence g (*) ii = p . (g,ii) by A19, A20, A15, CAT_1:def 1

.= the Comp of C . (gg,(id a9)) by A19, A20, A15, A4, A25, FUNCT_1:47

.= gg (*) (id a9) by A23, A24, CAT_1:16

.= g by A23, CAT_1:22 ;

:: thesis: verum

let g be Morphism of b,a; :: thesis: ii (*) g = g

reconsider gg = g as Morphism of C by A5;

A27: cod gg = cod g by A3, FUNCT_1:49

.= a9 by A15, A26, CAT_1:5 ;

A28: dom (id a9) = a9 ;

dom gg = dom g by A2, FUNCT_1:49

.= bb by A26, CAT_1:5 ;

then reconsider gg = gg as Morphism of bb,a9 by A27, CAT_1:4;

A29: cod g = a by A26, CAT_1:5;

hence ii (*) g = p . (ii,g) by A18, A20, A15, CAT_1:def 1

.= the Comp of C . ((id a9),gg) by A18, A20, A15, A4, A29, FUNCT_1:47

.= (id a9) (*) gg by A27, A28, CAT_1:16

.= g by A27, CAT_1:21 ;

:: thesis: verum

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, A8, RELAT_1:59;

hence CatStr(# O,M,d,c,p #) is Subcategory of C by A14, Def4; :: thesis: verum