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 A1, MCART_1:73; :: 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 A7, A6, A8, ZFMISC_1:96;

hence the Comp of D1 . x c= the Comp of D2 . x by A9, A10, GRFUNC_1:2; :: thesis: verum

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 A1, MCART_1:73; :: 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 A7, A6, A8, ZFMISC_1:96;

A10: now :: thesis: for y being object st y in dom c1 holds

c1 . y = c2 . y

( c1 = the Comp of D1 . x & c2 = the Comp of D2 . x )
by A5, MULTOP_1:def 1;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 A1, A4, Def11, MCART_1:69;

then A13: c2 c= c by A11, A12;

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 Def11, MULTOP_1:def 1;

then c1 c= c by A3, A5, A11;

hence c1 . y = c . y by A14, GRFUNC_1:2

.= c2 . y by A9, A14, A13, GRFUNC_1:2 ;

:: thesis: verum

end;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 A1, A4, Def11, MCART_1:69;

then A13: c2 c= c by A11, A12;

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 Def11, MULTOP_1:def 1;

then c1 c= c by A3, A5, A11;

hence c1 . y = c . y by A14, GRFUNC_1:2

.= c2 . y by A9, A14, A13, GRFUNC_1:2 ;

:: thesis: verum

hence the Comp of D1 . x c= the Comp of D2 . x by A9, A10, GRFUNC_1:2; :: thesis: verum