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

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

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

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;
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;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

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