let A be non empty reflexive AltCatStr ; for B being non empty reflexive SubCatStr of A
for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
let B be non empty reflexive SubCatStr of A; for C being non empty SubCatStr of A
for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
let C be non empty SubCatStr of A; for D being non empty SubCatStr of B st C = D holds
incl C = (incl B) * (incl D)
let D be non empty SubCatStr of B; ( C = D implies incl C = (incl B) * (incl D) )
assume A1:
C = D
; incl C = (incl B) * (incl D)
set X = [: the carrier of B, the carrier of B:];
set Y = [: the carrier of D, the carrier of D:];
A2:
the carrier of D c= the carrier of B
by ALTCAT_2:def 11;
then A3:
[: the carrier of D, the carrier of D:] c= [: the carrier of B, the carrier of B:]
by ZFMISC_1:96;
for i being object st i in [: the carrier of D, the carrier of D:] holds
the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i
proof
set dom2 =
dom the
MorphMap of
(incl D);
set dom1 =
dom ( the MorphMap of (incl B) * the ObjectMap of (incl D));
set XX = the
Arrows of
B;
set YY = the
Arrows of
D;
let i be
object ;
( i in [: the carrier of D, the carrier of D:] implies the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i )
A4:
the
MorphMap of
(incl C) . i = (id the Arrows of C) . i
by FUNCTOR0:def 28;
A5:
(
dom (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) = (dom the MorphMap of (incl D)) /\ (dom ( the MorphMap of (incl B) * the ObjectMap of (incl D))) &
dom the
MorphMap of
(incl D) = [: the carrier of D, the carrier of D:] )
by PARTFUN1:def 2, PBOOLE:def 19;
A6:
dom ( the MorphMap of (incl B) * the ObjectMap of (incl D)) =
dom ( the MorphMap of (incl B) * (id [: the carrier of D, the carrier of D:]))
by FUNCTOR0:def 28
.=
(dom the MorphMap of (incl B)) /\ [: the carrier of D, the carrier of D:]
by FUNCT_1:19
.=
[: the carrier of B, the carrier of B:] /\ [: the carrier of D, the carrier of D:]
by PARTFUN1:def 2
.=
[: the carrier of D, the carrier of D:]
by A2, XBOOLE_1:28, ZFMISC_1:96
;
assume A7:
i in [: the carrier of D, the carrier of D:]
;
the MorphMap of (incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i
then A8:
i in dom (id [: the carrier of D, the carrier of D:])
;
the
Arrows of
D cc= the
Arrows of
B
by ALTCAT_2:def 11;
then A9:
the
Arrows of
D . i c= the
Arrows of
B . i
by A7;
A10:
( the MorphMap of (incl B) * the ObjectMap of (incl D)) . i =
( the MorphMap of (incl B) * (id [: the carrier of D, the carrier of D:])) . i
by FUNCTOR0:def 28
.=
the
MorphMap of
(incl B) . ((id [: the carrier of D, the carrier of D:]) . i)
by A8, FUNCT_1:13
.=
the
MorphMap of
(incl B) . i
by A7, FUNCT_1:18
;
( the
MorphMap of
(incl B) . i = (id the Arrows of B) . i & the
MorphMap of
(incl D) . i = (id the Arrows of D) . i )
by FUNCTOR0:def 28;
then ( the MorphMap of (incl B) . i) * ( the MorphMap of (incl D) . i) =
((id the Arrows of B) . i) * (id ( the Arrows of D . i))
by A7, MSUALG_3:def 1
.=
(id ( the Arrows of B . i)) * (id ( the Arrows of D . i))
by A3, A7, MSUALG_3:def 1
.=
id (( the Arrows of B . i) /\ ( the Arrows of D . i))
by FUNCT_1:22
.=
id ( the Arrows of D . i)
by A9, XBOOLE_1:28
.=
the
MorphMap of
(incl C) . i
by A1, A7, A4, MSUALG_3:def 1
;
hence
the
MorphMap of
(incl C) . i = (( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i
by A7, A10, A5, A6, PBOOLE:def 19;
verum
end;
then A11:
the MorphMap of (incl C) = ( the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)
by A1, PBOOLE:3;
the ObjectMap of (incl C) =
id [: the carrier of D, the carrier of D:]
by A1, FUNCTOR0:def 28
.=
id ([: the carrier of B, the carrier of B:] /\ [: the carrier of D, the carrier of D:])
by A2, XBOOLE_1:28, ZFMISC_1:96
.=
(id [: the carrier of B, the carrier of B:]) * (id [: the carrier of D, the carrier of D:])
by FUNCT_1:22
.=
(id [: the carrier of B, the carrier of B:]) * the ObjectMap of (incl D)
by FUNCTOR0:def 28
.=
the ObjectMap of (incl B) * the ObjectMap of (incl D)
by FUNCTOR0:def 28
;
hence
incl C = (incl B) * (incl D)
by A1, A11, FUNCTOR0:def 36; verum