let C be AltCatStr ; :: thesis: for D being SubCatStr of C st the carrier of C = the carrier of D & the Arrows of C = the Arrows of D holds
D is full
let D be SubCatStr of C; :: thesis: ( the carrier of C = the carrier of D & the Arrows of C = the Arrows of D implies D is full )
assume that
A1: the carrier of C = the carrier of D and
A2: the Arrows of C = the Arrows of D ; :: thesis: D is full
dom the Arrows of C = [: the carrier of D, the carrier of D:] by A1, PARTFUN1:def 4;
hence the Arrows of D = the Arrows of C || the carrier of D by A2, RELAT_1:97; :: according to ALTCAT_2:def 13 :: thesis: verum