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

[: 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

( 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

A7:
dom the Arrows of A = [: the carrier of A, the carrier of A:]
by PARTFUN1:def 2;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;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

[: 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