let A be non empty AltCatStr ; :: thesis: for B being non empty SubCatStr of A holds

( B is full iff incl B is full )

let B be non empty SubCatStr of A; :: thesis: ( B is full iff incl B is full )

A5: the carrier of B c= the carrier of A by ALTCAT_2:def 11;

then A6: [: the carrier of B, the carrier of B:] c= [: the carrier of A, the carrier of A:] by ZFMISC_1:96;

dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def 2;

then A7: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by A5, XBOOLE_1:28, ZFMISC_1:96;

then dom ( the Arrows of A | [: the carrier of B, the carrier of B:]) = [: the carrier of B, the carrier of B:] by RELAT_1:61;

then reconsider XX = the Arrows of A || the carrier of B as ManySortedSet of [: the carrier of B, the carrier of B:] by PARTFUN1:def 2;

assume A8: incl B is full ; :: thesis: B is full

A9: XX c= the Arrows of B

( B is full iff incl B is full )

let B be non empty SubCatStr of A; :: thesis: ( B is full iff incl B is full )

hereby :: thesis: ( incl B is full implies B is full )

set I = [: the carrier of B, the carrier of B:];
ex I29 being non empty set ex B9 being ManySortedSet of I29 ex f9 being Function of [: the carrier of B, the carrier of B:],I29 st

( the ObjectMap of (incl B) = f9 & the Arrows of A = B9 & the MorphMap of (incl B) is ManySortedFunction of the Arrows of B,B9 * f9 ) by FUNCTOR0:def 3;

then reconsider f = the MorphMap of (incl B) as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (incl B) ;

set I = [: the carrier of B, the carrier of B:];

( the carrier of B c= the carrier of A & dom the Arrows of A = [: the carrier of A, the carrier of A:] ) by ALTCAT_2:def 11, PARTFUN1:def 2;

then A1: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by XBOOLE_1:28, ZFMISC_1:96;

assume A2: B is full ; :: thesis: incl B is full

f is "onto"

end;( the ObjectMap of (incl B) = f9 & the Arrows of A = B9 & the MorphMap of (incl B) is ManySortedFunction of the Arrows of B,B9 * f9 ) by FUNCTOR0:def 3;

then reconsider f = the MorphMap of (incl B) as ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (incl B) ;

set I = [: the carrier of B, the carrier of B:];

( the carrier of B c= the carrier of A & dom the Arrows of A = [: the carrier of A, the carrier of A:] ) by ALTCAT_2:def 11, PARTFUN1:def 2;

then A1: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by XBOOLE_1:28, ZFMISC_1:96;

assume A2: B is full ; :: thesis: incl B is full

f is "onto"

proof

hence
incl B is full
; :: thesis: verum
let i be set ; :: according to MSUALG_3:def 3 :: thesis: ( not i in [: the carrier of B, the carrier of B:] or rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i )

assume A3: i in [: the carrier of B, the carrier of B:] ; :: thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i

the Arrows of B = the Arrows of A || the carrier of B by A2;

then A4: the Arrows of B . i = the Arrows of A . i by A3, FUNCT_1:49;

rng (f . i) = rng ((id the Arrows of B) . i) by FUNCTOR0:def 28

.= rng (id ( the Arrows of B . i)) by A3, MSUALG_3:def 1

.= the Arrows of A . i by A4

.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by A1, A3, FUNCT_1:20

.= ( the Arrows of A * the ObjectMap of (incl B)) . i by FUNCTOR0:def 28 ;

hence rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i ; :: thesis: verum

end;assume A3: i in [: the carrier of B, the carrier of B:] ; :: thesis: rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i

the Arrows of B = the Arrows of A || the carrier of B by A2;

then A4: the Arrows of B . i = the Arrows of A . i by A3, FUNCT_1:49;

rng (f . i) = rng ((id the Arrows of B) . i) by FUNCTOR0:def 28

.= rng (id ( the Arrows of B . i)) by A3, MSUALG_3:def 1

.= the Arrows of A . i by A4

.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by A1, A3, FUNCT_1:20

.= ( the Arrows of A * the ObjectMap of (incl B)) . i by FUNCTOR0:def 28 ;

hence rng (f . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i ; :: thesis: verum

A5: the carrier of B c= the carrier of A by ALTCAT_2:def 11;

then A6: [: the carrier of B, the carrier of B:] c= [: the carrier of A, the carrier of A:] by ZFMISC_1:96;

dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def 2;

then A7: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by A5, XBOOLE_1:28, ZFMISC_1:96;

then dom ( the Arrows of A | [: the carrier of B, the carrier of B:]) = [: the carrier of B, the carrier of B:] by RELAT_1:61;

then reconsider XX = the Arrows of A || the carrier of B as ManySortedSet of [: the carrier of B, the carrier of B:] by PARTFUN1:def 2;

assume A8: incl B is full ; :: thesis: B is full

A9: XX c= the Arrows of B

proof

the Arrows of B c= XX
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in [: the carrier of B, the carrier of B:] or XX . i c= the Arrows of B . i )

assume A10: i in [: the carrier of B, the carrier of B:] ; :: thesis: XX . i c= the Arrows of B . i

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XX . i or x in the Arrows of B . i )

assume A11: x in XX . i ; :: thesis: x in the Arrows of B . i

x in the Arrows of B . i

end;assume A10: i in [: the carrier of B, the carrier of B:] ; :: thesis: XX . i c= the Arrows of B . i

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in XX . i or x in the Arrows of B . i )

assume A11: x in XX . i ; :: thesis: x in the Arrows of B . i

x in the Arrows of B . i

proof

hence
x in the Arrows of B . i
; :: thesis: verum
consider f being ManySortedFunction of the Arrows of B, the Arrows of A * the ObjectMap of (incl B) such that

A12: f = the MorphMap of (incl B) and

A13: f is "onto" by A8;

f = id the Arrows of B by A12, FUNCTOR0:def 28;

then A14: rng ((id the Arrows of B) . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i by A10, A13

.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by FUNCTOR0:def 28

.= the Arrows of A . i by A7, A10, FUNCT_1:20 ;

consider y, z being object such that

y in the carrier of A and

z in the carrier of A and

A15: i = [y,z] by A6, A10, ZFMISC_1:84;

( y in the carrier of B & z in the carrier of B ) by A10, A15, ZFMISC_1:87;

then A16: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5;

rng ((id the Arrows of B) . i) = rng (id ( the Arrows of B . i)) by A10, MSUALG_3:def 1

.= the Arrows of B . i ;

hence x in the Arrows of B . i by A11, A15, A16, A14; :: thesis: verum

end;A12: f = the MorphMap of (incl B) and

A13: f is "onto" by A8;

f = id the Arrows of B by A12, FUNCTOR0:def 28;

then A14: rng ((id the Arrows of B) . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i by A10, A13

.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by FUNCTOR0:def 28

.= the Arrows of A . i by A7, A10, FUNCT_1:20 ;

consider y, z being object such that

y in the carrier of A and

z in the carrier of A and

A15: i = [y,z] by A6, A10, ZFMISC_1:84;

( y in the carrier of B & z in the carrier of B ) by A10, A15, ZFMISC_1:87;

then A16: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5;

rng ((id the Arrows of B) . i) = rng (id ( the Arrows of B . i)) by A10, MSUALG_3:def 1

.= the Arrows of B . i ;

hence x in the Arrows of B . i by A11, A15, A16, A14; :: thesis: verum

proof

hence
the Arrows of B = the Arrows of A || the carrier of B
by A9, PBOOLE:146; :: according to ALTCAT_2:def 13 :: thesis: verum
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in [: the carrier of B, the carrier of B:] or the Arrows of B . i c= XX . i )

assume A17: i in [: the carrier of B, the carrier of B:] ; :: thesis: the Arrows of B . i c= XX . i

then consider y, z being object such that

y in the carrier of A and

z in the carrier of A and

A18: i = [y,z] by A6, ZFMISC_1:84;

( y in the carrier of B & z in the carrier of B ) by A17, A18, ZFMISC_1:87;

then A19: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Arrows of B . i or x in XX . i )

assume A20: x in the Arrows of B . i ; :: thesis: x in XX . i

the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;

then the Arrows of B . (y,z) c= the Arrows of A . (y,z) by A17, A18;

hence x in XX . i by A18, A20, A19; :: thesis: verum

end;assume A17: i in [: the carrier of B, the carrier of B:] ; :: thesis: the Arrows of B . i c= XX . i

then consider y, z being object such that

y in the carrier of A and

z in the carrier of A and

A18: i = [y,z] by A6, ZFMISC_1:84;

( y in the carrier of B & z in the carrier of B ) by A17, A18, ZFMISC_1:87;

then A19: XX . (y,z) = the Arrows of A . (y,z) by A5, ALTCAT_1:5;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Arrows of B . i or x in XX . i )

assume A20: x in the Arrows of B . i ; :: thesis: x in XX . i

the Arrows of B cc= the Arrows of A by ALTCAT_2:def 11;

then the Arrows of B . (y,z) c= the Arrows of A . (y,z) by A17, A18;

hence x in XX . i by A18, A20, A19; :: thesis: verum