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;

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

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;

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

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;

dom the Source of C = the carrier' of C 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:]

proof

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;

the Comp of C c= the Comp of A by CAT_2:def 4;
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