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 )

assume A1: B is full ; :: thesis: incl B is full
set I = [:the carrier of B,the carrier of B:];
A2: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
dom the Arrows of A = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then A3: (dom the Arrows of A) /\ [:the carrier of B,the carrier of B:] = [:the carrier of B,the carrier of B:] by A2, XBOOLE_1:28, ZFMISC_1:119;
consider I2' being non empty set , B' being ManySortedSet of , f' being Function of [:the carrier of B,the carrier of B:],I2' such that
A4: the ObjectMap of (incl B) = f' and
A5: ( the Arrows of A = B' & the MorphMap of (incl B) is ManySortedFunction of the Arrows of B,B' * f' ) by FUNCTOR0:def 4;
reconsider f = the MorphMap of (incl B) as ManySortedFunction of the Arrows of B,the Arrows of A * the ObjectMap of (incl B) by A4, A5;
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 A6: i in [:the carrier of B,the carrier of B:] ; :: thesis: rng (f . i) = (the Arrows of A * the ObjectMap of (incl B)) . i
A7: the Arrows of B . i = the Arrows of A . i

proof

the Arrows of B = the Arrows of A || the carrier of B by A1, ALTCAT_2:def 13;
hence the Arrows of B . i = the Arrows of A . i by A6, FUNCT_1:72; :: thesis: verum

end;

rng (f . i) = rng ((id the Arrows of B) . i) by FUNCTOR0:def 29
.= rng (id (the Arrows of B . i)) by A6, MSUALG_3:def 1
.= the Arrows of A . i by A7, RELAT_1:71
.= (the Arrows of A * (id [:the carrier of B,the carrier of B:])) . i by A3, A6, FUNCT_1:38
.= (the Arrows of A * the ObjectMap of (incl B)) . i by FUNCTOR0:def 29 ;
hence rng (f . i) = (the Arrows of A * the ObjectMap of (incl B)) . i ; :: thesis: verum

end;

hence incl B is full by FUNCTOR0:def 33; :: thesis: verum

end;

assume A8: incl B is full ; :: thesis: B is full
set I = [:the carrier of B,the carrier of B:];
A9: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
then A10: [:the carrier of B,the carrier of B:] c= [:the carrier of A,the carrier of A:] by ZFMISC_1:119;
dom the Arrows of A = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;
then A11: (dom the Arrows of A) /\ [:the carrier of B,the carrier of B:] = [:the carrier of B,the carrier of B:] by A9, XBOOLE_1:28, ZFMISC_1:119;
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:90;
then reconsider XX = the Arrows of A || the carrier of B as ManySortedSet of by PARTFUN1:def 4;
the Arrows of B = XX

proof

thus the Arrows of B c= XX :: according to PBOOLE:def 13 :: thesis: XX c= the Arrows of B

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in [:the carrier of B,the carrier of B:] or the Arrows of B . i c= XX . i )
assume A12: i in [:the carrier of B,the carrier of B:] ; :: thesis: the Arrows of B . i c= XX . i
then consider y, z being set such that
A13: ( y in the carrier of A & z in the carrier of A & i = [y,z] ) by A10, ZFMISC_1:103;
A14: ( y in the carrier of B & z in the carrier of B ) by A12, A13, ZFMISC_1:106;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Arrows of B . i or x in XX . i )
assume A15: 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 A16: the Arrows of B . y,z c= the Arrows of A . y,z by A12, A13, ALTCAT_2:def 2;
XX . y,z = the Arrows of A . y,z by A9, A14, ALTCAT_1:7;
hence x in XX . i by A13, A15, A16; :: thesis: verum

end;

thus XX c= the Arrows of B :: thesis: verum

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in [:the carrier of B,the carrier of B:] or XX . i c= the Arrows of B . i )
assume A17: i in [:the carrier of B,the carrier of B:] ; :: thesis: XX . i c= the Arrows of B . i
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in XX . i or x in the Arrows of B . i )
assume A18: x in XX . i ; :: thesis: x in the Arrows of B . i
x in the Arrows of B . i

proof

consider y, z being set such that
A19: ( y in the carrier of A & z in the carrier of A & i = [y,z] ) by A10, A17, ZFMISC_1:103;
( y in the carrier of B & z in the carrier of B ) by A17, A19, ZFMISC_1:106;
then A20: XX . y,z = the Arrows of A . y,z by A9, ALTCAT_1:7;
consider f being ManySortedFunction of the Arrows of B,the Arrows of A * the ObjectMap of (incl B) such that
A21: ( f = the MorphMap of (incl B) & f is "onto" ) by A8, FUNCTOR0:def 33;
f = id the Arrows of B by A21, FUNCTOR0:def 29;
then A22: rng ((id the Arrows of B) . i) = (the Arrows of A * the ObjectMap of (incl B)) . i by A17, A21, MSUALG_3:def 3
.= (the Arrows of A * (id [:the carrier of B,the carrier of B:])) . i by FUNCTOR0:def 29
.= the Arrows of A . i by A11, A17, FUNCT_1:38 ;
rng ((id the Arrows of B) . i) = rng (id (the Arrows of B . i)) by A17, MSUALG_3:def 1
.= the Arrows of B . i by RELAT_1:71 ;
hence x in the Arrows of B . i by A18, A19, A20, A22; :: thesis: verum

end;

hence x in the Arrows of B . i ; :: thesis: verum

end;

end;

hence the Arrows of B = the Arrows of A || the carrier of B ; :: according to ALTCAT_2:def 13 :: thesis: verum