set M = MSSCat A;
set G = MSSCat A;
thus MSSCat A is transitive :: thesis:

proof

let o1, o2, o3 be object of (MSSCat A); :: according to ALTCAT_1:def 4 :: thesis:
reconsider o19 = o1, o29 = o2, o39 = o3 as Element of MSS_set A by Def1;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; :: thesis:
consider s being Element of MSS_morph o29,o39;
MSS_morph o29,o39 <> {} by A2, Def1;
then consider u, w being Function such that
s = [u,w] and
A3: u,w form_morphism_between o29,o39 by MSALIMIT:def 10;
consider t being Element of MSS_morph o19,o29;
MSS_morph o19,o29 <> {} by A1, Def1;
then consider f, g being Function such that
t = [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:30;
then [(u * f),(w * g)] in MSS_morph o19,o39 by MSALIMIT:def 10;
hence not <^o1,o3^> = {} by Def1; :: thesis:

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:

proof

let i, j, k, l be Element of (MSSCat A); :: according to ALTCAT_1:def 7 :: thesis:
reconsider I = i, J = j, K = k, L = l as object of (MSSCat A) ;
let f, g, h be set ; :: thesis:
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 ; :: thesis:
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:30;
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: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 i9,k9 by A11, A9, PUA2MSS1:30;
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; :: thesis:

end;

thus the Comp of (MSSCat A) is with_left_units :: according to ALTCAT_1:def 18 :: thesis:

proof

let j be Element of (MSSCat A); :: according to ALTCAT_1:def 9 :: thesis:
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;
take e = [(id the carrier of j9),(id the carrier' of j9)]; :: thesis:
( 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:29;
hence A22: e in the Arrows of (MSSCat A) . j,j by MSALIMIT:def 10; :: thesis:
let i be Element of (MSSCat A); :: thesis:
reconsider i9 = i as Element of MSS_set A by Def1;
let f be set ; :: thesis:
reconsider I = i, J = j as object of (MSSCat A) ;
assume A23: f in the Arrows of (MSSCat A) . i,j ; :: thesis:
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 13;
rng f1 c= the carrier of j9 by A25, PUA2MSS1:def 13;
then A27: (id the carrier of j9) * f1 = f1 by RELAT_1:79;
(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:79; :: thesis:

end;

thus the Comp of (MSSCat A) is with_right_units :: thesis:

proof

let i be Element of (MSSCat A); :: according to ALTCAT_1:def 8 :: thesis:
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;
take e = [(id the carrier of i9),(id the carrier' of i9)]; :: thesis:
( 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:29;
hence A28: e in the Arrows of (MSSCat A) . i,i by MSALIMIT:def 10; :: thesis:
let j be Element of (MSSCat A); :: thesis:
reconsider j9 = j as Element of MSS_set A by Def1;
let f be set ; :: thesis:
reconsider I = i, J = j as object of (MSSCat A) ;
assume A29: f in the Arrows of (MSSCat A) . i,j ; :: thesis:
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 13;
dom f1 = the carrier of i9 by A31, PUA2MSS1:def 13;
then A33: f1 * (id the carrier of i9) = f1 by RELAT_1:78;
(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:78; :: thesis:

end;