let C be non empty transitive AltCatStr ; 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; ( 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
; D1 is SubCatStr of D2
thus
the carrier of D1 c= the carrier of D2
by A1; ALTCAT_2:def 11 ( 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; 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; ALTCAT_2:def 2 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 ; ( 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:]
; 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 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 ;
( 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
;
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
;
verum
( c1 = the Comp of D1 . x & c2 = the Comp of D2 . x )
by A5, MULTOP_1:def 1;
hence
the Comp of D1 . x c= the Comp of D2 . x
by A9, A10, GRFUNC_1:2; verum