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 & the Id of C = the Id 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 & the Id of C = the Id of A | the carrier of C )
A1: dom the Source of A = the carrier' of A by FUNCT_2:def 1;

A2: now

let x be set ; :: 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:14;
thus the Source of C . x = dom m
.= dom m9 by CAT_2:15
.= the Source of A . x ; :: thesis: verum

end;

A3: now

let x be set ; :: 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:14;
thus the Target of C . x = cod m
.= cod m9 by CAT_2:15
.= 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:13, XBOOLE_1:28;
hence the Source of C = the Source of A | the carrier' of C by A2, FUNCT_1:68; :: 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 & the Id of C = the Id 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:13, XBOOLE_1:28;
hence the Target of C = the Target of A | the carrier' of C by A3, FUNCT_1:68; :: thesis: ( the Comp of C = the Comp of A || the carrier' of C & the Id of C = the Id 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:25;
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 set ; :: 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 A8: 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:14;
x in dom the Comp of A by A7, XBOOLE_0:def 4;
then A9: [f9,g9] in dom the Comp of A by MCART_1:23;
dom f = dom f9 by CAT_2:15
.= cod g9 by A9, CAT_1:40
.= cod g by CAT_2:15 ;
then [f,g] in dom the Comp of C by CAT_1:40;
hence x in dom the Comp of C by A8, MCART_1:23; :: 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:64
.= ( the Comp of A | (dom the Comp of A)) | [: the carrier' of C, the carrier' of C:] by RELAT_1:100
.= the Comp of A || the carrier' of C by RELAT_1:97 ;
:: thesis: the Id of C = the Id of A | the carrier of C
A10: dom the Id of A = the carrier of A by FUNCT_2:def 1;
A11: the carrier of C c= the carrier of A by CAT_2:def 4;

A12: now

let x be set ; :: thesis: ( x in dom the Id of C implies the Id of C . x = the Id of A . x )
assume x in dom the Id of C ; :: thesis: the Id of C . x = the Id of A . x
then reconsider o = x as Object of C by FUNCT_2:def 1;
reconsider o9 = o as Object of A by CAT_2:12;
thus the Id of C . x = id o
.= id o9 by CAT_2:def 4
.= the Id of A . x ; :: thesis: verum

end;

dom the Id of C = the carrier of C by FUNCT_2:def 1;
then dom the Id of C = (dom the Id of A) /\ the carrier of C by A10, A11, XBOOLE_1:28;
hence the Id of C = the Id of A | the carrier of C by A12, FUNCT_1:68; :: thesis: verum