let A be Category; 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; ( 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;
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; ( 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; 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;
XBOOLE_0:def 10 (dom the Comp of A) /\ [: the carrier' of C, the carrier' of C:] c= dom the Comp of C
let x be
object ;
TARSKI:def 3 ( 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:]
;
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;
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
;
verum