set M = MSSCat A;

set G = MSSCat A;

thus MSSCat A is transitive :: thesis: ( MSSCat A is associative & MSSCat A is with_units )

set C = the Comp of (MSSCat A);

thus the Comp of (MSSCat A) is associative :: according to ALTCAT_1:def 15 :: thesis: MSSCat A is with_units

set G = MSSCat A;

thus MSSCat A is transitive :: thesis: ( MSSCat A is associative & MSSCat A is with_units )

proof

set G = the Arrows of (MSSCat A);
let o1, o2, o3 be Object of (MSSCat A); :: 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 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; :: thesis: verum

end;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 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; :: thesis: verum

set C = the Comp of (MSSCat A);

thus the Comp of (MSSCat A) is associative :: according to ALTCAT_1:def 15 :: thesis: MSSCat A is with_units

proof

thus
the Comp of (MSSCat A) is with_left_units
:: according to ALTCAT_1:def 16 :: thesis: the Comp of (MSSCat A) is with_right_units
let i, j, k, l be Element of (MSSCat A); :: according to ALTCAT_1:def 5 :: thesis: for b_{1}, b_{2}, b_{3} being set holds

( not b_{1} in the Arrows of (MSSCat A) . (i,j) or not b_{2} in the Arrows of (MSSCat A) . (j,k) or not b_{3} in the Arrows of (MSSCat A) . (k,l) or ( the Comp of (MSSCat A) . (i,k,l)) . (b_{3},(( the Comp of (MSSCat A) . (i,j,k)) . (b_{2},b_{1}))) = ( the Comp of (MSSCat A) . (i,j,l)) . ((( the Comp of (MSSCat A) . (j,k,l)) . (b_{3},b_{2})),b_{1}) )

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 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: ( 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; :: thesis: verum

end;( not b

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 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: ( 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; :: thesis: verum

proof

thus
the Comp of (MSSCat A) is with_right_units
:: thesis: verum
let j be Element of (MSSCat A); :: according to ALTCAT_1:def 7 :: thesis: ex b_{1} being set st

( b_{1} in the Arrows of (MSSCat A) . (j,j) & ( for b_{2} being Element of the carrier of (MSSCat A)

for b_{3} being set holds

( not b_{3} in the Arrows of (MSSCat A) . (b_{2},j) or ( the Comp of (MSSCat A) . (b_{2},j,j)) . (b_{1},b_{3}) = b_{3} ) ) )

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 (MSSCat A) . (j,j) & ( for b_{1} being Element of the carrier of (MSSCat A)

for b_{2} being set holds

( not b_{2} in the Arrows of (MSSCat A) . (b_{1},j) or ( the Comp of (MSSCat A) . (b_{1},j,j)) . (e,b_{2}) = b_{2} ) ) )

( 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; :: thesis: for b_{1} being Element of the carrier of (MSSCat A)

for b_{2} being set holds

( not b_{2} in the Arrows of (MSSCat A) . (b_{1},j) or ( the Comp of (MSSCat A) . (b_{1},j,j)) . (e,b_{2}) = b_{2} )

let i be Element of (MSSCat A); :: thesis: for b_{1} being set holds

( not b_{1} in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,j,j)) . (e,b_{1}) = b_{1} )

reconsider i9 = 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 (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; :: thesis: verum

end;( b

for b

( not b

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 (MSSCat A) . (j,j) & ( for b

for b

( not b

( 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; :: thesis: for b

for b

( not b

let i be Element of (MSSCat A); :: thesis: for b

( not b

reconsider i9 = 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 (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; :: thesis: verum

proof

let i be Element of (MSSCat A); :: according to ALTCAT_1:def 6 :: thesis: ex b_{1} being set st

( b_{1} in the Arrows of (MSSCat A) . (i,i) & ( for b_{2} being Element of the carrier of (MSSCat A)

for b_{3} being set holds

( not b_{3} in the Arrows of (MSSCat A) . (i,b_{2}) or ( the Comp of (MSSCat A) . (i,i,b_{2})) . (b_{3},b_{1}) = b_{3} ) ) )

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 (MSSCat A) . (i,i) & ( for b_{1} being Element of the carrier of (MSSCat A)

for b_{2} being set holds

( not b_{2} in the Arrows of (MSSCat A) . (i,b_{1}) or ( the Comp of (MSSCat A) . (i,i,b_{1})) . (b_{2},e) = b_{2} ) ) )

( 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; :: thesis: for b_{1} being Element of the carrier of (MSSCat A)

for b_{2} being set holds

( not b_{2} in the Arrows of (MSSCat A) . (i,b_{1}) or ( the Comp of (MSSCat A) . (i,i,b_{1})) . (b_{2},e) = b_{2} )

let j be Element of (MSSCat A); :: thesis: for b_{1} being set holds

( not b_{1} in the Arrows of (MSSCat A) . (i,j) or ( the Comp of (MSSCat A) . (i,i,j)) . (b_{1},e) = b_{1} )

reconsider j9 = 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 (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; :: thesis: verum

end;( b

for b

( not b

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 (MSSCat A) . (i,i) & ( for b

for b

( not b

( 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; :: thesis: for b

for b

( not b

let j be Element of (MSSCat A); :: thesis: for b

( not b

reconsider j9 = 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 (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; :: thesis: verum