let A be Category; :: thesis: for C being Subcategory of A holds

( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

let C be Subcategory of A; :: thesis: ( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

A1: dom the Source of A = the carrier' of A by FUNCT_2:def 1;

then dom the Source of C = (dom the Source of A) /\ the carrier' of C by A1, CAT_2:7, XBOOLE_1:28;

hence the Source of C = the Source of A | the carrier' of C by A2, FUNCT_1:46; :: thesis: ( the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

A4: dom the Target of A = the carrier' of A by FUNCT_2:def 1;

dom the Target of C = the carrier' of C by FUNCT_2:def 1;

then dom the Target of C = (dom the Target of A) /\ the carrier' of C by A4, CAT_2:7, XBOOLE_1:28;

hence the Target of C = the Target of A | the carrier' of C by A3, FUNCT_1:46; :: thesis: the Comp of C = the Comp of A || the carrier' of C

A5: dom the Comp of C = (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:]

hence the Comp of C = the Comp of A | ((dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:]) by A5, GRFUNC_1:23

.= ( the Comp of A | (dom the Comp of A)) | [: the carrier' of C, the carrier' of C:] by RELAT_1:71

.= the Comp of A || the carrier' of C ;

:: thesis: verum

( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

let C be Subcategory of A; :: thesis: ( the Source of C = the Source of A | the carrier' of C & the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

A1: dom the Source of A = the carrier' of A by FUNCT_2:def 1;

A2: now :: thesis: for x being object st x in dom the Source of C holds

the Source of C . x = the Source of A . x

the Source of C . x = the Source of A . x

let x be object ; :: thesis: ( x in dom the Source of C implies the Source of C . x = the Source of A . x )

assume x in dom the Source of C ; :: thesis: the Source of C . x = the Source of A . x

then reconsider m = x as Morphism of C by FUNCT_2:def 1;

reconsider m9 = m as Morphism of A by CAT_2:8;

thus the Source of C . x = dom m

.= dom m9 by CAT_2:9

.= the Source of A . x ; :: thesis: verum

end;assume x in dom the Source of C ; :: thesis: the Source of C . x = the Source of A . x

then reconsider m = x as Morphism of C by FUNCT_2:def 1;

reconsider m9 = m as Morphism of A by CAT_2:8;

thus the Source of C . x = dom m

.= dom m9 by CAT_2:9

.= the Source of A . x ; :: thesis: verum

A3: now :: thesis: for x being object st x in dom the Target of C holds

the Target of C . x = the Target of A . x

dom the Source of C = the carrier' of C
by FUNCT_2:def 1;the Target of C . x = the Target of A . x

let x be object ; :: thesis: ( x in dom the Target of C implies the Target of C . x = the Target of A . x )

assume x in dom the Target of C ; :: thesis: the Target of C . x = the Target of A . x

then reconsider m = x as Morphism of C by FUNCT_2:def 1;

reconsider m9 = m as Morphism of A by CAT_2:8;

thus the Target of C . x = cod m

.= cod m9 by CAT_2:9

.= the Target of A . x ; :: thesis: verum

end;assume x in dom the Target of C ; :: thesis: the Target of C . x = the Target of A . x

then reconsider m = x as Morphism of C by FUNCT_2:def 1;

reconsider m9 = m as Morphism of A by CAT_2:8;

thus the Target of C . x = cod m

.= cod m9 by CAT_2:9

.= the Target of A . x ; :: thesis: verum

then dom the Source of C = (dom the Source of A) /\ the carrier' of C by A1, CAT_2:7, XBOOLE_1:28;

hence the Source of C = the Source of A | the carrier' of C by A2, FUNCT_1:46; :: thesis: ( the Target of C = the Target of A | the carrier' of C & the Comp of C = the Comp of A || the carrier' of C )

A4: dom the Target of A = the carrier' of A by FUNCT_2:def 1;

dom the Target of C = the carrier' of C by FUNCT_2:def 1;

then dom the Target of C = (dom the Target of A) /\ the carrier' of C by A4, CAT_2:7, XBOOLE_1:28;

hence the Target of C = the Target of A | the carrier' of C by A3, FUNCT_1:46; :: thesis: the Comp of C = the Comp of A || the carrier' of C

A5: dom the Comp of C = (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:]

proof

the Comp of C c= the Comp of A
by CAT_2:def 4;
the Comp of C c= the Comp of A
by CAT_2:def 4;

then A6: dom the Comp of C c= dom the Comp of A by RELAT_1:11;

dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def 18;

hence dom the Comp of C c= (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] by A6, XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] c= dom the Comp of C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] or x in dom the Comp of C )

assume A7: x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] ; :: thesis: x in dom the Comp of C

then x in [: the carrier' of C, the carrier' of C:] by XBOOLE_0:def 4;

then reconsider f = x `1 , g = x `2 as Morphism of C by MCART_1:10;

reconsider f9 = f, g9 = g as Morphism of A by CAT_2:8;

x in dom the Comp of A by A7, XBOOLE_0:def 4;

then A8: [f9,g9] in dom the Comp of A by MCART_1:21;

dom f = dom f9 by CAT_2:9

.= cod g9 by A8, CAT_1:15

.= cod g by CAT_2:9 ;

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

hence x in dom the Comp of C by A7, MCART_1:21; :: thesis: verum

end;then A6: dom the Comp of C c= dom the Comp of A by RELAT_1:11;

dom the Comp of C c= [: the carrier' of C, the carrier' of C:] by RELAT_1:def 18;

hence dom the Comp of C c= (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] by A6, XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] c= dom the Comp of C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] or x in dom the Comp of C )

assume A7: x in (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] ; :: thesis: x in dom the Comp of C

then x in [: the carrier' of C, the carrier' of C:] by XBOOLE_0:def 4;

then reconsider f = x `1 , g = x `2 as Morphism of C by MCART_1:10;

reconsider f9 = f, g9 = g as Morphism of A by CAT_2:8;

x in dom the Comp of A by A7, XBOOLE_0:def 4;

then A8: [f9,g9] in dom the Comp of A by MCART_1:21;

dom f = dom f9 by CAT_2:9

.= cod g9 by A8, CAT_1:15

.= cod g by CAT_2:9 ;

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

hence x in dom the Comp of C by A7, MCART_1:21; :: thesis: verum

hence the Comp of C = the Comp of A | ((dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:]) by A5, GRFUNC_1:23

.= ( the Comp of A | (dom the Comp of A)) | [: the carrier' of C, the carrier' of C:] by RELAT_1:71

.= the Comp of A || the carrier' of C ;

:: thesis: verum