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:29; :: 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 )
assume A1: 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
A2: the carrier of B c= the carrier of A by ALTCAT_2:def 11;
then A3: [: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 XBOOLE_1:28, ZFMISC_1:119;
A4: ( dom the Arrows of A = [:the carrier of A,the carrier of A:] & dom the Arrows of B = [:the carrier of B,the carrier of B:] ) by PARTFUN1:def 4;

now

let x be set ; :: 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 set such that
A5: ( b1 in the carrier of B & b2 in the carrier of B & x = [b1,b2] ) by A4, 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 A2, A5;
thus the Arrows of B . x = <^b1,b2^> by A5
.= <^a1,a2^> by A1
.= the Arrows of A . x by A5 ; :: thesis: verum

end;

hence the Arrows of B = the Arrows of A || the carrier of B by A3, A4, FUNCT_1:68; :: according to ALTCAT_2:def 13 :: thesis: verum