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 (); :: according to ALTCAT_1:def 2 :: thesis: ( <^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^> <> {} ; :: thesis: not <^o1,o3^> = {}
set s = the Element of MSS_morph (o29,o39);
MSS_morph (o29,o39) <> {} by ;
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 ;
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 ;
then [(u * f),(w * g)] in MSS_morph (o19,o39) by MSALIMIT:def 10;
hence not <^o1,o3^> = {} by Def1; :: thesis: verum
end;
set G = the Arrows of ();
set C = the Comp of ();
thus the Comp of () is associative :: according to ALTCAT_1:def 15 :: thesis:
proof
let i, j, k, l be Element of (); :: according to ALTCAT_1:def 5 :: thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of () . (i,j) or not b2 in the Arrows of () . (j,k) or not b3 in the Arrows of () . (k,l) or ( the Comp of () . (i,k,l)) . (b3,(( the Comp of () . (i,j,k)) . (b2,b1))) = ( the Comp of () . (i,j,l)) . ((( the Comp of () . (j,k,l)) . (b3,b2)),b1) )

reconsider I = i, J = j, K = k, L = l as Object of () ;
let f, g, h be set ; :: thesis: ( not f in the Arrows of () . (i,j) or not g in the Arrows of () . (j,k) or not h in the Arrows of () . (k,l) or ( the Comp of () . (i,k,l)) . (h,(( the Comp of () . (i,j,k)) . (g,f))) = ( the Comp of () . (i,j,l)) . ((( the Comp of () . (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 () . (i,j) and
A6: g in the Arrows of () . (j,k) and
A7: h in the Arrows of () . (k,l) ; :: thesis: ( the Comp of () . (i,k,l)) . (h,(( the Comp of () . (i,j,k)) . (g,f))) = ( the Comp of () . (i,j,l)) . ((( the Comp of () . (j,k,l)) . (h,g)),f)
g in MSS_morph (j9,k9) by ;
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 ;
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 () . (i,j,k)) . (g,f) = [(g1 * f1),(g2 * f2)] by A5, A6, A10, A11, A8, A9, Def1;
h in MSS_morph (k9,l9) by ;
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 () . (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 ;
then [(h1 * g1),(h2 * g2)] in MSS_morph (j9,l9) by MSALIMIT:def 10;
then A16: [(h1 * g1),(h2 * g2)] in the Arrows of () . (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 () ;
then A18: J in MSS_set A by Def1;
L in the carrier of () ;
then A19: L in MSS_set A by Def1;
g1 * f1,g2 * f2 form_morphism_between i9,k9 by ;
then [(g1 * f1),(g2 * f2)] in MSS_morph (i9,k9) by MSALIMIT:def 10;
then A20: [(g1 * f1),(g2 * f2)] in the Arrows of () . (i,k) by Def1;
I in the carrier of () ;
then A21: I in MSS_set A by Def1;
K in the carrier of () ;
then K in MSS_set A by Def1;
then ( the Comp of () . (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 () . (i,k,l)) . (h,(( the Comp of () . (i,j,k)) . (g,f))) = ( the Comp of () . (i,j,l)) . ((( the Comp of () . (j,k,l)) . (h,g)),f) by A21, A18, A19, A5, A10, A12, A15, A16, A17, Def1; :: thesis: verum
end;
thus the Comp of () is with_left_units :: according to ALTCAT_1:def 16 :: thesis: the Comp of () is with_right_units
proof
let j be Element of (); :: according to ALTCAT_1:def 7 :: thesis: ex b1 being set st
( b1 in the Arrows of () . (j,j) & ( for b2 being Element of the carrier of ()
for b3 being set holds
( not b3 in the Arrows of () . (b2,j) or ( the Comp of () . (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 ; :: thesis: ( e in the Arrows of () . (j,j) & ( for b1 being Element of the carrier of ()
for b2 being set holds
( not b2 in the Arrows of () . (b1,j) or ( the Comp of () . (b1,j,j)) . (e,b2) = b2 ) ) )

( id the carrier of j9, id the carrier' of j9 form_morphism_between j9,j9 & the Arrows of () . (j,j) = MSS_morph (j9,j9) ) by ;
hence A22: e in the Arrows of () . (j,j) by MSALIMIT:def 10; :: thesis: for b1 being Element of the carrier of ()
for b2 being set holds
( not b2 in the Arrows of () . (b1,j) or ( the Comp of () . (b1,j,j)) . (e,b2) = b2 )

let i be Element of (); :: thesis: for b1 being set holds
( not b1 in the Arrows of () . (i,j) or ( the Comp of () . (i,j,j)) . (e,b1) = b1 )

reconsider i9 = i as Element of MSS_set A by Def1;
let f be set ; :: thesis: ( not f in the Arrows of () . (i,j) or ( the Comp of () . (i,j,j)) . (e,f) = f )
reconsider I = i, J = j as Object of () ;
assume A23: f in the Arrows of () . (i,j) ; :: thesis: ( the Comp of () . (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 ;
rng f1 c= the carrier of j9 by ;
then A27: (id the carrier of j9) * f1 = f1 by RELAT_1:53;
( the Comp of () . (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 () . (i,j,j)) . (e,f) = f by ; :: thesis: verum
end;
thus the Comp of () is with_right_units :: thesis: verum
proof
let i be Element of (); :: according to ALTCAT_1:def 6 :: thesis: ex b1 being set st
( b1 in the Arrows of () . (i,i) & ( for b2 being Element of the carrier of ()
for b3 being set holds
( not b3 in the Arrows of () . (i,b2) or ( the Comp of () . (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 ; :: thesis: ( e in the Arrows of () . (i,i) & ( for b1 being Element of the carrier of ()
for b2 being set holds
( not b2 in the Arrows of () . (i,b1) or ( the Comp of () . (i,i,b1)) . (b2,e) = b2 ) ) )

( id the carrier of i9, id the carrier' of i9 form_morphism_between i9,i9 & the Arrows of () . (i,i) = MSS_morph (i9,i9) ) by ;
hence A28: e in the Arrows of () . (i,i) by MSALIMIT:def 10; :: thesis: for b1 being Element of the carrier of ()
for b2 being set holds
( not b2 in the Arrows of () . (i,b1) or ( the Comp of () . (i,i,b1)) . (b2,e) = b2 )

let j be Element of (); :: thesis: for b1 being set holds
( not b1 in the Arrows of () . (i,j) or ( the Comp of () . (i,i,j)) . (b1,e) = b1 )

reconsider j9 = j as Element of MSS_set A by Def1;
let f be set ; :: thesis: ( not f in the Arrows of () . (i,j) or ( the Comp of () . (i,i,j)) . (f,e) = f )
reconsider I = i, J = j as Object of () ;
assume A29: f in the Arrows of () . (i,j) ; :: thesis: ( the Comp of () . (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 ;
dom f1 = the carrier of i9 by ;
then A33: f1 * (id the carrier of i9) = f1 by RELAT_1:52;
( the Comp of () . (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 () . (i,i,j)) . (f,e) = f by ; :: thesis: verum
end;