set M = MSSCat A;
set G = MSSCat A;
thus
MSSCat A is transitive
:: thesis: ( MSSCat A is associative & MSSCat A is with_units )proof
let o1,
o2,
o3 be
object of
(MSSCat A);
:: according to ALTCAT_1:def 4 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o1' =
o1,
o2' =
o2,
o3' =
o3 as
Element of
MSS_set A by Def1;
assume that A1:
<^o1,o2^> <> {}
and A2:
<^o2,o3^> <> {}
;
:: thesis: not <^o1,o3^> = {}
consider s being
Element of
MSS_morph o2',
o3';
MSS_morph o2',
o3' <> {}
by A2, Def1;
then consider u,
w being
Function such that
s = [u,w]
and A3:
u,
w form_morphism_between o2',
o3'
by MSALIMIT:def 10;
consider t being
Element of
MSS_morph o1',
o2';
MSS_morph o1',
o2' <> {}
by A1, Def1;
then consider f,
g being
Function such that
t = [f,g]
and A4:
f,
g form_morphism_between o1',
o2'
by MSALIMIT:def 10;
u * f,
w * g form_morphism_between o1',
o3'
by A4, A3, PUA2MSS1:30;
then
[(u * f),(w * g)] in MSS_morph o1',
o3'
by MSALIMIT:def 10;
hence
not
<^o1,o3^> = {}
by Def1;
:: thesis: verum
end;
set G = the Arrows of (MSSCat A);
set C = the Comp of (MSSCat A);
thus
the Comp of (MSSCat A) is associative
:: according to ALTCAT_1:def 17 :: thesis: MSSCat A is with_units proof
let i,
j,
k,
l be
Element of
(MSSCat A);
:: according to ALTCAT_1:def 7 :: thesis: 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 ;
:: thesis: ( 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 i' =
i,
j' =
j,
k' =
k,
l' =
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
;
:: thesis: (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 j',
k'
by A6, Def1;
then consider g1,
g2 being
Function such that A8:
g = [g1,g2]
and A9:
g1,
g2 form_morphism_between j',
k'
by MSALIMIT:def 10;
f in MSS_morph i',
j'
by A5, Def1;
then consider f1,
f2 being
Function such that A10:
f = [f1,f2]
and A11:
f1,
f2 form_morphism_between i',
j'
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 k',
l'
by A7, Def1;
then consider h1,
h2 being
Function such that A13:
h = [h1,h2]
and A14:
h1,
h2 form_morphism_between k',
l'
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 j',
l'
by A9, A14, PUA2MSS1:30;
then
[(h1 * g1),(h2 * g2)] in MSS_morph j',
l'
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:55;
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 i',
k'
by A11, A9, PUA2MSS1:30;
then
[(g1 * f1),(g2 * f2)] in MSS_morph i',
k'
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;
:: thesis: verum
end;
thus
the Comp of (MSSCat A) is with_left_units
:: according to ALTCAT_1:def 18 :: thesis: the Comp of (MSSCat A) is with_right_units proof
let j be
Element of
(MSSCat A);
:: according to ALTCAT_1:def 9 :: thesis: 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 j' =
j as
Element of
MSS_set A by Def1;
set e1 =
id the
carrier of
j';
set e2 =
id the
carrier' of
j';
take e =
[(id the carrier of j'),(id the carrier' of j')];
:: thesis: ( 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
j',
id the
carrier' of
j' form_morphism_between j',
j' & the
Arrows of
(MSSCat A) . j,
j = MSS_morph j',
j' )
by Def1, PUA2MSS1:29;
hence A22:
e in the
Arrows of
(MSSCat A) . j,
j
by MSALIMIT:def 10;
:: thesis: 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);
:: thesis: 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 i' =
i as
Element of
MSS_set A by Def1;
let f be
set ;
:: thesis: ( 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
;
:: thesis: (the Comp of (MSSCat A) . i,j,j) . e,f = f
then
f in MSS_morph i',
j'
by Def1;
then consider f1,
f2 being
Function such that A24:
f = [f1,f2]
and A25:
f1,
f2 form_morphism_between i',
j'
by MSALIMIT:def 10;
A26:
rng f2 c= the
carrier' of
j'
by A25, PUA2MSS1:def 13;
rng f1 c= the
carrier of
j'
by A25, PUA2MSS1:def 13;
then A27:
(id the carrier of j') * f1 = f1
by RELAT_1:79;
(the Comp of (MSSCat A) . I,J,J) . [(id the carrier of j'),(id the carrier' of j')],
[f1,f2] = [((id the carrier of j') * f1),((id the carrier' of j') * 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:79;
:: thesis: verum
end;
thus
the Comp of (MSSCat A) is with_right_units
:: thesis: verumproof
let i be
Element of
(MSSCat A);
:: according to ALTCAT_1:def 8 :: thesis: 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 i' =
i as
Element of
MSS_set A by Def1;
set e1 =
id the
carrier of
i';
set e2 =
id the
carrier' of
i';
take e =
[(id the carrier of i'),(id the carrier' of i')];
:: thesis: ( 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
i',
id the
carrier' of
i' form_morphism_between i',
i' & the
Arrows of
(MSSCat A) . i,
i = MSS_morph i',
i' )
by Def1, PUA2MSS1:29;
hence A28:
e in the
Arrows of
(MSSCat A) . i,
i
by MSALIMIT:def 10;
:: thesis: 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);
:: thesis: 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 j' =
j as
Element of
MSS_set A by Def1;
let f be
set ;
:: thesis: ( 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
;
:: thesis: (the Comp of (MSSCat A) . i,i,j) . f,e = f
then
f in MSS_morph i',
j'
by Def1;
then consider f1,
f2 being
Function such that A30:
f = [f1,f2]
and A31:
f1,
f2 form_morphism_between i',
j'
by MSALIMIT:def 10;
A32:
dom f2 = the
carrier' of
i'
by A31, PUA2MSS1:def 13;
dom f1 = the
carrier of
i'
by A31, PUA2MSS1:def 13;
then A33:
f1 * (id the carrier of i') = f1
by RELAT_1:78;
(the Comp of (MSSCat A) . I,I,J) . [f1,f2],
[(id the carrier of i'),(id the carrier' of i')] = [(f1 * (id the carrier of i')),(f2 * (id the carrier' of i'))]
by A28, A29, A30, A31, Def1;
hence
(the Comp of (MSSCat A) . i,i,j) . f,
e = f
by A30, A32, A33, RELAT_1:78;
:: thesis: verum
end;