set M = MSSCat A;
set G = MSSCat A;
thus
MSSCat A is transitive
( MSSCat A is associative & MSSCat A is with_units )proof
let o1,
o2,
o3 be
Object of
(MSSCat A);
ALTCAT_1:def 2 ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o19 =
o1,
o29 =
o2,
o39 =
o3 as
Element of
MSS_set A by Def1;
assume that A1:
<^o1,o2^> <> {}
and A2:
<^o2,o3^> <> {}
;
not <^o1,o3^> = {}
set s = the
Element of
MSS_morph (
o29,
o39);
MSS_morph (
o29,
o39)
<> {}
by A2, Def1;
then consider u,
w being
Function such that
the
Element of
MSS_morph (
o29,
o39)
= [u,w]
and A3:
u,
w form_morphism_between o29,
o39
by MSALIMIT:def 10;
set t = the
Element of
MSS_morph (
o19,
o29);
MSS_morph (
o19,
o29)
<> {}
by A1, Def1;
then consider f,
g being
Function such that
the
Element of
MSS_morph (
o19,
o29)
= [f,g]
and A4:
f,
g form_morphism_between o19,
o29
by MSALIMIT:def 10;
u * f,
w * g form_morphism_between o19,
o39
by A4, A3, PUA2MSS1:29;
then
[(u * f),(w * g)] in MSS_morph (
o19,
o39)
by MSALIMIT:def 10;
hence
not
<^o1,o3^> = {}
by Def1;
verum
end;
set G = the Arrows of (MSSCat A);
set C = the Comp of (MSSCat A);
thus
the Comp of (MSSCat A) is associative
ALTCAT_1:def 15 MSSCat A is with_units proof
let i,
j,
k,
l be
Element of
(MSSCat A);
ALTCAT_1:def 5 for b1, b2, b3 being set holds
( not b1 in the Arrows of (MSSCat A) . (i,j) or not b2 in the Arrows of (MSSCat A) . (j,k) or not b3 in the Arrows of (MSSCat A) . (k,l) or ( the Comp of (MSSCat A) . (i,k,l)) . (b3,(( the Comp of (MSSCat A) . (i,j,k)) . (b2,b1))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (b3,b2)),b1) )
reconsider I =
i,
J =
j,
K =
k,
L =
l as
Object of
(MSSCat A) ;
let f,
g,
h be
set ;
( not f in the Arrows of (MSSCat A) . (i,j) or not g in the Arrows of (MSSCat A) . (j,k) or not h in the Arrows of (MSSCat A) . (k,l) or ( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f) )
reconsider i9 =
i,
j9 =
j,
k9 =
k,
l9 =
l as
Element of
MSS_set A by Def1;
assume that A5:
f in the
Arrows of
(MSSCat A) . (
i,
j)
and A6:
g in the
Arrows of
(MSSCat A) . (
j,
k)
and A7:
h in the
Arrows of
(MSSCat A) . (
k,
l)
;
( the Comp of (MSSCat A) . (i,k,l)) . (h,(( the Comp of (MSSCat A) . (i,j,k)) . (g,f))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),f)
g in MSS_morph (
j9,
k9)
by A6, Def1;
then consider g1,
g2 being
Function such that A8:
g = [g1,g2]
and A9:
g1,
g2 form_morphism_between j9,
k9
by MSALIMIT:def 10;
f in MSS_morph (
i9,
j9)
by A5, Def1;
then consider f1,
f2 being
Function such that A10:
f = [f1,f2]
and A11:
f1,
f2 form_morphism_between i9,
j9
by MSALIMIT:def 10;
A12:
( the Comp of (MSSCat A) . (i,j,k)) . (
g,
f)
= [(g1 * f1),(g2 * f2)]
by A5, A6, A10, A11, A8, A9, Def1;
h in MSS_morph (
k9,
l9)
by A7, Def1;
then consider h1,
h2 being
Function such that A13:
h = [h1,h2]
and A14:
h1,
h2 form_morphism_between k9,
l9
by MSALIMIT:def 10;
A15:
( the Comp of (MSSCat A) . (j,k,l)) . (
h,
g)
= [(h1 * g1),(h2 * g2)]
by A6, A7, A8, A9, A13, A14, Def1;
h1 * g1,
h2 * g2 form_morphism_between j9,
l9
by A9, A14, PUA2MSS1:29;
then
[(h1 * g1),(h2 * g2)] in MSS_morph (
j9,
l9)
by MSALIMIT:def 10;
then A16:
[(h1 * g1),(h2 * g2)] in the
Arrows of
(MSSCat A) . (
j,
l)
by Def1;
A17:
(
(h1 * g1) * f1 = h1 * (g1 * f1) &
(h2 * g2) * f2 = h2 * (g2 * f2) )
by RELAT_1:36;
J in the
carrier of
(MSSCat A)
;
then A18:
J in MSS_set A
by Def1;
L in the
carrier of
(MSSCat A)
;
then A19:
L in MSS_set A
by Def1;
g1 * f1,
g2 * f2 form_morphism_between i9,
k9
by A11, A9, PUA2MSS1:29;
then
[(g1 * f1),(g2 * f2)] in MSS_morph (
i9,
k9)
by MSALIMIT:def 10;
then A20:
[(g1 * f1),(g2 * f2)] in the
Arrows of
(MSSCat A) . (
i,
k)
by Def1;
I in the
carrier of
(MSSCat A)
;
then A21:
I in MSS_set A
by Def1;
K in the
carrier of
(MSSCat A)
;
then
K in MSS_set A
by Def1;
then
( the Comp of (MSSCat A) . (i,k,l)) . (
h,
[(g1 * f1),(g2 * f2)])
= [(h1 * (g1 * f1)),(h2 * (g2 * f2))]
by A21, A19, A7, A13, A20, Def1;
hence
( the Comp of (MSSCat A) . (i,k,l)) . (
h,
(( the Comp of (MSSCat A) . (i,j,k)) . (g,f)))
= ( the Comp of (MSSCat A) . (i,j,l)) . (
(( the Comp of (MSSCat A) . (j,k,l)) . (h,g)),
f)
by A21, A18, A19, A5, A10, A12, A15, A16, A17, Def1;
verum
end;
thus
the Comp of (MSSCat A) is with_left_units
ALTCAT_1:def 16 the Comp of (MSSCat A) is with_right_units proof
let j be
Element of
(MSSCat A);
ALTCAT_1:def 7 ex b1 being set st
( b1 in the Arrows of (MSSCat A) . (j,j) & ( for b2 being Element of the carrier of (MSSCat A)
for b3 being set holds
( not b3 in the Arrows of (MSSCat A) . (b2,j) or ( the Comp of (MSSCat A) . (b2,j,j)) . (b1,b3) = b3 ) ) )
reconsider j9 =
j as
Element of
MSS_set A by Def1;
set e1 =
id the
carrier of
j9;
set e2 =
id the
carrier' of
j9;
reconsider e =
[(id the carrier of j9),(id the carrier' of j9)] as
set ;
take
e
;
( e in the Arrows of (MSSCat A) . (j,j) & ( for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (b1,j) or ( the Comp of (MSSCat A) . (b1,j,j)) . (e,b2) = b2 ) ) )
(
id the
carrier of
j9,
id the
carrier' of
j9 form_morphism_between j9,
j9 & the
Arrows of
(MSSCat A) . (
j,
j)
= MSS_morph (
j9,
j9) )
by Def1, PUA2MSS1:28;
hence A22:
e in the
Arrows of
(MSSCat A) . (
j,
j)
by MSALIMIT:def 10;
for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (b1,j) or ( the Comp of (MSSCat A) . (b1,j,j)) . (e,b2) = b2 )
let i be
Element of
(MSSCat A);
for b1 being set holds
( not b1 in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,j,j)) . (e,b1) = b1 )
reconsider i9 =
i as
Element of
MSS_set A by Def1;
let f be
set ;
( not f in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f )
reconsider I =
i,
J =
j as
Object of
(MSSCat A) ;
assume A23:
f in the
Arrows of
(MSSCat A) . (
i,
j)
;
( the Comp of (MSSCat A) . (i,j,j)) . (e,f) = f
then
f in MSS_morph (
i9,
j9)
by Def1;
then consider f1,
f2 being
Function such that A24:
f = [f1,f2]
and A25:
f1,
f2 form_morphism_between i9,
j9
by MSALIMIT:def 10;
A26:
rng f2 c= the
carrier' of
j9
by A25, PUA2MSS1:def 12;
rng f1 c= the
carrier of
j9
by A25, PUA2MSS1:def 12;
then A27:
(id the carrier of j9) * f1 = f1
by RELAT_1:53;
( the Comp of (MSSCat A) . (I,J,J)) . (
[(id the carrier of j9),(id the carrier' of j9)],
[f1,f2])
= [((id the carrier of j9) * f1),((id the carrier' of j9) * f2)]
by A22, A23, A24, A25, Def1;
hence
( the Comp of (MSSCat A) . (i,j,j)) . (
e,
f)
= f
by A24, A26, A27, RELAT_1:53;
verum
end;
thus
the Comp of (MSSCat A) is with_right_units
verumproof
let i be
Element of
(MSSCat A);
ALTCAT_1:def 6 ex b1 being set st
( b1 in the Arrows of (MSSCat A) . (i,i) & ( for b2 being Element of the carrier of (MSSCat A)
for b3 being set holds
( not b3 in the Arrows of (MSSCat A) . (i,b2) or ( the Comp of (MSSCat A) . (i,i,b2)) . (b3,b1) = b3 ) ) )
reconsider i9 =
i as
Element of
MSS_set A by Def1;
set e1 =
id the
carrier of
i9;
set e2 =
id the
carrier' of
i9;
reconsider e =
[(id the carrier of i9),(id the carrier' of i9)] as
set ;
take
e
;
( e in the Arrows of (MSSCat A) . (i,i) & ( for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (i,b1) or ( the Comp of (MSSCat A) . (i,i,b1)) . (b2,e) = b2 ) ) )
(
id the
carrier of
i9,
id the
carrier' of
i9 form_morphism_between i9,
i9 & the
Arrows of
(MSSCat A) . (
i,
i)
= MSS_morph (
i9,
i9) )
by Def1, PUA2MSS1:28;
hence A28:
e in the
Arrows of
(MSSCat A) . (
i,
i)
by MSALIMIT:def 10;
for b1 being Element of the carrier of (MSSCat A)
for b2 being set holds
( not b2 in the Arrows of (MSSCat A) . (i,b1) or ( the Comp of (MSSCat A) . (i,i,b1)) . (b2,e) = b2 )
let j be
Element of
(MSSCat A);
for b1 being set holds
( not b1 in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,i,j)) . (b1,e) = b1 )
reconsider j9 =
j as
Element of
MSS_set A by Def1;
let f be
set ;
( not f in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f )
reconsider I =
i,
J =
j as
Object of
(MSSCat A) ;
assume A29:
f in the
Arrows of
(MSSCat A) . (
i,
j)
;
( the Comp of (MSSCat A) . (i,i,j)) . (f,e) = f
then
f in MSS_morph (
i9,
j9)
by Def1;
then consider f1,
f2 being
Function such that A30:
f = [f1,f2]
and A31:
f1,
f2 form_morphism_between i9,
j9
by MSALIMIT:def 10;
A32:
dom f2 = the
carrier' of
i9
by A31, PUA2MSS1:def 12;
dom f1 = the
carrier of
i9
by A31, PUA2MSS1:def 12;
then A33:
f1 * (id the carrier of i9) = f1
by RELAT_1:52;
( the Comp of (MSSCat A) . (I,I,J)) . (
[f1,f2],
[(id the carrier of i9),(id the carrier' of i9)])
= [(f1 * (id the carrier of i9)),(f2 * (id the carrier' of i9))]
by A28, A29, A30, A31, Def1;
hence
( the Comp of (MSSCat A) . (i,i,j)) . (
f,
e)
= f
by A30, A32, A33, RELAT_1:52;
verum
end;