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 )
hereby :: thesis: ( incl B is full implies B is full )
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 ;
then A1: (dom the Arrows of A) /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by ;
assume A2: B is full ; :: thesis: incl B is full
f is "onto"
proof
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 ;
rng (f . i) = rng ((id the Arrows of B) . i) by FUNCTOR0:def 28
.= rng (id ( the Arrows of B . i)) by
.= the Arrows of A . i by A4
.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by
.= ( 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;
hence incl B is full ; :: thesis: verum
end;
set I = [: the carrier of B, the carrier of B:];
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 ;
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
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
proof
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 ;
then A14: rng ((id the Arrows of B) . i) = ( the Arrows of A * the ObjectMap of (incl B)) . i by
.= ( the Arrows of A * (id [: the carrier of B, the carrier of B:])) . i by FUNCTOR0:def 28
.= the Arrows of A . i by ;
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 ;
( y in the carrier of B & z in the carrier of B ) by ;
then A16: XX . (y,z) = the Arrows of A . (y,z) by ;
rng ((id the Arrows of B) . i) = rng (id ( the Arrows of B . i)) by
.= the Arrows of B . i ;
hence x in the Arrows of B . i by A11, A15, A16, A14; :: thesis: verum
end;
hence x in the Arrows of B . i ; :: thesis: verum
end;
the Arrows of B c= XX
proof
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 ;
( y in the carrier of B & z in the carrier of B ) by ;
then A19: XX . (y,z) = the Arrows of A . (y,z) by ;
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 ;
hence x in XX . i by ; :: thesis: verum
end;
hence the Arrows of B = the Arrows of A || the carrier of B by ; :: according to ALTCAT_2:def 13 :: thesis: verum