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:119;
for i being set 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
set ;
( 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 29;
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 4, PBOOLE:def 24;
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 29
.=
(dom the MorphMap of (incl B)) /\ [:the carrier of D,the carrier of D:]
by FUNCT_1:37
.=
[:the carrier of B,the carrier of B:] /\ [:the carrier of D,the carrier of D:]
by PARTFUN1:def 4
.=
[:the carrier of D,the carrier of D:]
by A2, XBOOLE_1:28, ZFMISC_1:119
;
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:])
by FUNCT_1:34;
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, ALTCAT_2:def 2;
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 29
.=
the
MorphMap of
(incl B) . ((id [:the carrier of D,the carrier of D:]) . i)
by A8, FUNCT_1:23
.=
the
MorphMap of
(incl B) . i
by A7, FUNCT_1:35
;
( 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 29;
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:43
.=
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 24;
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 29
.=
id ([:the carrier of B,the carrier of B:] /\ [:the carrier of D,the carrier of D:])
by A2, XBOOLE_1:28, ZFMISC_1:119
.=
(id [:the carrier of B,the carrier of B:]) * (id [:the carrier of D,the carrier of D:])
by FUNCT_1:43
.=
(id [:the carrier of B,the carrier of B:]) * the ObjectMap of (incl D)
by FUNCTOR0:def 29
.=
the ObjectMap of (incl B) * the ObjectMap of (incl D)
by FUNCTOR0:def 29
;
hence
incl C = (incl B) * (incl D)
by A1, A11, FUNCTOR0:def 37; verum