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: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 ; :: 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 )
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:] ; :: thesis: 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; :: thesis: 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; :: thesis: verum