let C be non empty transitive AltCatStr ; :: thesis: for D1, D2 being non empty transitive SubCatStr of C st the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 holds
D1 is SubCatStr of D2

let D1, D2 be non empty transitive SubCatStr of C; :: thesis: ( the carrier of D1 c= the carrier of D2 & the Arrows of D1 cc= the Arrows of D2 implies D1 is SubCatStr of D2 )
assume that
A1: the carrier of D1 c= the carrier of D2 and
A2: the Arrows of D1 cc= the Arrows of D2 ; :: thesis: D1 is SubCatStr of D2
thus the carrier of D1 c= the carrier of D2 by A1; :: according to ALTCAT_2:def 11 :: thesis: ( the Arrows of D1 cc= the Arrows of D2 & the Comp of D1 cc= the Comp of D2 )
thus the Arrows of D1 cc= the Arrows of D2 by A2; :: thesis: the Comp of D1 cc= the Comp of D2
thus [: the carrier of D1, the carrier of D1, the carrier of D1:] c= [: the carrier of D2, the carrier of D2, the carrier of D2:] by ; :: according to ALTCAT_2:def 2 :: thesis: for i being set st i in [: the carrier of D1, the carrier of D1, the carrier of D1:] holds
the Comp of D1 . i c= the Comp of D2 . i

let x be set ; :: thesis: ( x in [: the carrier of D1, the carrier of D1, the carrier of D1:] implies the Comp of D1 . x c= the Comp of D2 . x )
assume A3: x in [: the carrier of D1, the carrier of D1, the carrier of D1:] ; :: thesis: the Comp of D1 . x c= the Comp of D2 . x
then consider i1, i2, i3 being object such that
A4: ( i1 in the carrier of D1 & i2 in the carrier of D1 & i3 in the carrier of D1 ) and
A5: x = [i1,i2,i3] by MCART_1:68;
reconsider i1 = i1, i2 = i2, i3 = i3 as Object of D1 by A4;
reconsider j1 = i1, j2 = i2, j3 = i3 as Object of D2 by A1;
[i2,i3] in [: the carrier of D1, the carrier of D1:] ;
then A6: <^i2,i3^> c= <^j2,j3^> by A2;
reconsider c2 = the Comp of D2 . (j1,j2,j3) as Function of [:<^j2,j3^>,<^j1,j2^>:],<^j1,j3^> ;
reconsider c1 = the Comp of D1 . (i1,i2,i3) as Function of [:<^i2,i3^>,<^i1,i2^>:],<^i1,i3^> ;
( not <^i1,i3^> = {} or <^i2,i3^> = {} or <^i1,i2^> = {} ) by ALTCAT_1:def 2;
then ( <^i1,i3^> = {} implies [:<^i2,i3^>,<^i1,i2^>:] = {} ) by ZFMISC_1:90;
then A7: dom c1 = [:<^i2,i3^>,<^i1,i2^>:] by FUNCT_2:def 1;
( not <^j1,j3^> = {} or <^j2,j3^> = {} or <^j1,j2^> = {} ) by ALTCAT_1:def 2;
then ( <^j1,j3^> = {} implies [:<^j2,j3^>,<^j1,j2^>:] = {} ) by ZFMISC_1:90;
then A8: dom c2 = [:<^j2,j3^>,<^j1,j2^>:] by FUNCT_2:def 1;
[i1,i2] in [: the carrier of D1, the carrier of D1:] ;
then <^i1,i2^> c= <^j1,j2^> by A2;
then A9: dom c1 c= dom c2 by ;
A10: now :: thesis: for y being object st y in dom c1 holds
c1 . y = c2 . y
the carrier of D1 c= the carrier of C by Def11;
then reconsider o1 = i1, o2 = i2, o3 = i3 as Object of C ;
reconsider c = the Comp of C . (o1,o2,o3) as Function of [:<^o2,o3^>,<^o1,o2^>:],<^o1,o3^> ;
let y be object ; :: thesis: ( y in dom c1 implies c1 . y = c2 . y )
A11: c = the Comp of C . [o1,o2,o3] by MULTOP_1:def 1;
A12: c2 = the Comp of D2 . [o1,o2,o3] by MULTOP_1:def 1;
( [o1,o2,o3] in [: the carrier of D2, the carrier of D2, the carrier of D2:] & the Comp of D2 cc= the Comp of C ) by ;
then A13: c2 c= c by ;
assume A14: y in dom c1 ; :: thesis: c1 . y = c2 . y
( the Comp of D1 cc= the Comp of C & c1 = the Comp of D1 . [o1,o2,o3] ) by ;
then c1 c= c by A3, A5, A11;
hence c1 . y = c . y by
.= c2 . y by ;
:: thesis: verum
end;
( c1 = the Comp of D1 . x & c2 = the Comp of D2 . x ) by ;
hence the Comp of D1 . x c= the Comp of D2 . x by ; :: thesis: verum