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:77; :: 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 set 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:72;
reconsider i1 = i1, i2 = i2, i3 = i3 as object of D1 by A4;
( not <^i1,i3^> = {} or <^i2,i3^> = {} or <^i1,i2^> = {} )
by ALTCAT_1:def 4;
then A6:
( <^i1,i3^> = {} implies [:<^i2,i3^>,<^i1,i2^>:] = {} )
by ZFMISC_1:113;
reconsider c1 = the Comp of D1 . i1,i2,i3 as Function of [:<^i2,i3^>,<^i1,i2^>:],<^i1,i3^> ;
A7:
dom c1 = [:<^i2,i3^>,<^i1,i2^>:]
by A6, FUNCT_2:def 1;
reconsider j1 = i1, j2 = i2, j3 = i3 as object of D2 by A1, A4;
( not <^j1,j3^> = {} or <^j2,j3^> = {} or <^j1,j2^> = {} )
by ALTCAT_1:def 4;
then A8:
( <^j1,j3^> = {} implies [:<^j2,j3^>,<^j1,j2^>:] = {} )
by ZFMISC_1:113;
reconsider c2 = the Comp of D2 . j1,j2,j3 as Function of [:<^j2,j3^>,<^j1,j2^>:],<^j1,j3^> ;
( [i1,i2] in [:the carrier of D1,the carrier of D1:] & [i2,i3] in [:the carrier of D1,the carrier of D1:] )
;
then A9:
( <^i1,i2^> c= <^j1,j2^> & <^i2,i3^> c= <^j2,j3^> )
by A2, Def2;
dom c2 = [:<^j2,j3^>,<^j1,j2^>:]
by A8, FUNCT_2:def 1;
then A10:
dom c1 c= dom c2
by A7, A9, ZFMISC_1:119;
A11:
now let y be
set ;
:: thesis: ( y in dom c1 implies 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 by A4;
reconsider c = the
Comp of
C . o1,
o2,
o3 as
Function of
[:<^o2,o3^>,<^o1,o2^>:],
<^o1,o3^> ;
A12:
c = the
Comp of
C . [o1,o2,o3]
by MULTOP_1:def 1;
A13:
[o1,o2,o3] in [:the carrier of D2,the carrier of D2,the carrier of D2:]
by A1, A4, MCART_1:73;
assume A14:
y in dom c1
;
:: thesis: c1 . y = c2 . yA15:
the
Comp of
D2 cc= the
Comp of
C
by Def11;
c2 = the
Comp of
D2 . [o1,o2,o3]
by MULTOP_1:def 1;
then A16:
c2 c= c
by A12, A13, A15, Def2;
A17:
the
Comp of
D1 cc= the
Comp of
C
by Def11;
c1 = the
Comp of
D1 . [o1,o2,o3]
by MULTOP_1:def 1;
then
c1 c= c
by A3, A5, A12, A17, Def2;
hence c1 . y =
c . y
by A14, GRFUNC_1:8
.=
c2 . y
by A10, A14, A16, GRFUNC_1:8
;
:: thesis: verum end;
( 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 A10, A11, GRFUNC_1:8; :: thesis: verum