let A be non empty reflexive AltCatStr ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( C = D implies incl C = (incl B) * (incl D) )
assume A1: C = D ; :: thesis: 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;
A4: 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 ;
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

let i be set ; :: thesis: ( 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 )
assume A5: i in [:the carrier of D,the carrier of D:] ; :: thesis: the MorphMap of (incl C) . i = ((the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i
then A6: i in dom (id [:the carrier of D,the carrier of D:]) by FUNCT_1:34;
set XX = the Arrows of B;
set YY = the Arrows of D;
the Arrows of D cc= the Arrows of B by ALTCAT_2:def 11;
then A7: the Arrows of D . i c= the Arrows of B . i by A5, ALTCAT_2:def 2;
A8: the MorphMap of (incl C) . i = (the MorphMap of (incl B) . i) * (the MorphMap of (incl D) . i)

proof

A9: the MorphMap of (incl B) . i = (id the Arrows of B) . i by FUNCTOR0:def 29;
A10: the MorphMap of (incl D) . i = (id the Arrows of D) . i by FUNCTOR0:def 29;
A11: the MorphMap of (incl C) . i = (id the Arrows of C) . i by FUNCTOR0:def 29;
(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 A5, A9, A10, MSUALG_3:def 1
.= (id (the Arrows of B . i)) * (id (the Arrows of D . i)) by A3, A5, 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 A7, XBOOLE_1:28
.= the MorphMap of (incl C) . i by A1, A5, A11, MSUALG_3:def 1 ;
hence the MorphMap of (incl C) . i = (the MorphMap of (incl B) . i) * (the MorphMap of (incl D) . i) ; :: thesis: verum

end;

A12: (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 A6, FUNCT_1:23
.= the MorphMap of (incl B) . i by A5, FUNCT_1:35 ;
set dom1 = dom (the MorphMap of (incl B) * the ObjectMap of (incl D));
set dom2 = dom the MorphMap of (incl D);
A13: 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))) by PBOOLE:def 24;
i in (dom the MorphMap of (incl D)) /\ (dom (the MorphMap of (incl B) * the ObjectMap of (incl D)))

proof

A14: dom the MorphMap of (incl D) = [:the carrier of D,the carrier of D:] by PARTFUN1:def 4;
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 ;
hence i in (dom the MorphMap of (incl D)) /\ (dom (the MorphMap of (incl B) * the ObjectMap of (incl D))) by A5, A14; :: thesis: verum

end;

hence the MorphMap of (incl C) . i = ((the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D)) . i by A8, A12, A13, PBOOLE:def 24; :: thesis: verum

end;

then the MorphMap of (incl C) = (the MorphMap of (incl B) * the ObjectMap of (incl D)) ** the MorphMap of (incl D) by A1, PBOOLE:3;
hence incl C = (incl B) * (incl D) by A1, A4, FUNCTOR0:def 37; :: thesis: verum