let A be non empty AltCatStr ; :: thesis: for B being non empty SubCatStr of A holds
( B is full iff for a1, a2 being Object of A
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )
let B be non empty SubCatStr of A; :: thesis: ( B is full iff for a1, a2 being Object of A
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> )
thus ( B is full implies for a1, a2 being Object of A
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> ) by ALTCAT_2:28; :: thesis: ( ( for a1, a2 being Object of A
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> ) implies B is full )
A1: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
A2: dom the Arrows of B = [: the carrier of B, the carrier of B:] by PARTFUN1:def 2;
assume A3: for a1, a2 being Object of A
for b1, b2 being Object of B st b1 = a1 & b2 = a2 holds
<^b1,b2^> = <^a1,a2^> ; :: thesis: B is full

A4: now :: thesis: for x being object st x in dom the Arrows of B holds
the Arrows of B . x = the Arrows of A . x

let x be object ; :: thesis: ( x in dom the Arrows of B implies the Arrows of B . x = the Arrows of A . x )
assume x in dom the Arrows of B ; :: thesis: the Arrows of B . x = the Arrows of A . x
then consider b1, b2 being object such that
A5: ( b1 in the carrier of B & b2 in the carrier of B ) and
A6: x = [b1,b2] by ZFMISC_1:def 2;
reconsider b1 = b1, b2 = b2 as Object of B by A5;
reconsider a1 = b1, a2 = b2 as Object of A by A1;
thus the Arrows of B . x = <^b1,b2^> by A6
.= <^a1,a2^> by A3
.= the Arrows of A . x by A6 ; :: thesis: verum

end;

A7: dom the Arrows of A = [: the carrier of A, the carrier of A:] by PARTFUN1:def 2;
[: the carrier of A, the carrier of A:] /\ [: the carrier of B, the carrier of B:] = [: the carrier of B, the carrier of B:] by A1, XBOOLE_1:28, ZFMISC_1:96;
hence the Arrows of B = the Arrows of A || the carrier of B by A7, A2, A4, FUNCT_1:46; :: according to ALTCAT_2:def 13 :: thesis: verum