set M = MSAlgCat (S,A);
set G = MSAlgCat (S,A);
set GM = the Arrows of (MSAlgCat (S,A));
set C = the Comp of (MSAlgCat (S,A));
thus MSAlgCat (S,A) is transitive :: thesis: ( MSAlgCat (S,A) is associative & MSAlgCat (S,A) is with_units )
proof
let o1, o2, o3 be Object of (MSAlgCat (S,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 MSAlg_set (S,A) by Def4;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}
set t = the Element of MSAlg_morph (S,A,o19,o29);
MSAlg_morph (S,A,o19,o29) <> {} by ;
then consider M, N being strict feasible MSAlgebra over S, f being ManySortedFunction of M,N such that
A3: M = o19 and
A4: N = o29 and
f = the Element of MSAlg_morph (S,A,o19,o29) and
A5: the Sorts of M is_transformable_to the Sorts of N and
A6: f is_homomorphism M,N by Def3;
set s = the Element of MSAlg_morph (S,A,o29,o39);
MSAlg_morph (S,A,o29,o39) <> {} by ;
then consider M1, N1 being strict feasible MSAlgebra over S, g being ManySortedFunction of M1,N1 such that
A7: M1 = o29 and
A8: N1 = o39 and
g = the Element of MSAlg_morph (S,A,o29,o39) and
A9: the Sorts of M1 is_transformable_to the Sorts of N1 and
A10: g is_homomorphism M1,N1 by Def3;
reconsider g9 = g as ManySortedFunction of N,N1 by A4, A7;
consider GF being ManySortedFunction of M,N1 such that
GF = g9 ** f and
A11: GF is_homomorphism M,N1 by A4, A5, A6, A7, A9, A10, Th5;
the Sorts of M is_transformable_to the Sorts of N1 by ;
then GF in MSAlg_morph (S,A,o19,o39) by A3, A8, A11, Def3;
hence not <^o1,o3^> = {} by Def4; :: thesis: verum
end;
thus the Comp of (MSAlgCat (S,A)) is associative :: according to ALTCAT_1:def 15 :: thesis: MSAlgCat (S,A) is with_units
proof
let i, j, k, l be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def 5 :: thesis: for b1, b2, b3 being set holds
( not b1 in the Arrows of (MSAlgCat (S,A)) . (i,j) or not b2 in the Arrows of (MSAlgCat (S,A)) . (j,k) or not b3 in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (b3,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (b2,b1))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (b3,b2)),b1) )

let f, g, h be set ; :: thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or not g in the Arrows of (MSAlgCat (S,A)) . (j,k) or not h in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) )
reconsider i9 = i, j9 = j, k9 = k, l9 = l as Element of MSAlg_set (S,A) by Def4;
assume that
A12: f in the Arrows of (MSAlgCat (S,A)) . (i,j) and
A13: g in the Arrows of (MSAlgCat (S,A)) . (j,k) and
A14: h in the Arrows of (MSAlgCat (S,A)) . (k,l) ; :: thesis: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f)
g in MSAlg_morph (S,A,j9,k9) by ;
then consider M2, N2 being strict feasible MSAlgebra over S, G being ManySortedFunction of M2,N2 such that
A15: M2 = j9 and
A16: N2 = k9 and
A17: g = G and
A18: the Sorts of M2 is_transformable_to the Sorts of N2 and
A19: G is_homomorphism M2,N2 by Def3;
h in MSAlg_morph (S,A,k9,l9) by ;
then consider M3, N3 being strict feasible MSAlgebra over S, H being ManySortedFunction of M3,N3 such that
A20: M3 = k9 and
A21: N3 = l9 and
A22: h = H and
A23: the Sorts of M3 is_transformable_to the Sorts of N3 and
A24: H is_homomorphism M3,N3 by Def3;
reconsider G9 = G as ManySortedFunction of M2,M3 by ;
consider HG being ManySortedFunction of M2,N3 such that
A25: HG = H ** G9 and
A26: HG is_homomorphism M2,N3 by A16, A18, A19, A20, A23, A24, Th5;
A27: ( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (H,G) = H ** G9 by A13, A14, A17, A22, Def4;
f in MSAlg_morph (S,A,i9,j9) by ;
then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that
A28: M1 = i9 and
A29: N1 = j9 and
A30: f = F and
A31: the Sorts of M1 is_transformable_to the Sorts of N1 and
A32: F is_homomorphism M1,N1 by Def3;
A33: ( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f) = G ** F by A12, A13, A30, A17, Def4;
consider GF being ManySortedFunction of M1,M3 such that
A34: GF = G9 ** F and
A35: GF is_homomorphism M1,M3 by A29, A31, A32, A15, A16, A18, A19, A20, Th5;
the Sorts of M1 is_transformable_to the Sorts of M3 by ;
then G9 ** F in MSAlg_morph (S,A,i9,k9) by A28, A20, A34, A35, Def3;
then GF in the Arrows of (MSAlgCat (S,A)) . (i,k) by ;
then A36: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (H,GF) = H ** GF by ;
the Sorts of M2 is_transformable_to the Sorts of N3 by ;
then HG in MSAlg_morph (S,A,j9,l9) by ;
then A37: H ** G9 in the Arrows of (MSAlgCat (S,A)) . (j,l) by ;
(H ** G9) ** F = H ** (G9 ** F) by PBOOLE:140;
hence ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (h,(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (g,f))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (h,g)),f) by A12, A30, A17, A22, A33, A34, A36, A27, A37, Def4; :: thesis: verum
end;
thus the Comp of (MSAlgCat (S,A)) is with_left_units :: according to ALTCAT_1:def 16 :: thesis: the Comp of (MSAlgCat (S,A)) is with_right_units
proof
let j be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def 7 :: thesis: ex b1 being set st
( b1 in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b2 being Element of the carrier of (MSAlgCat (S,A))
for b3 being set holds
( not b3 in the Arrows of (MSAlgCat (S,A)) . (b2,j) or ( the Comp of (MSAlgCat (S,A)) . (b2,j,j)) . (b1,b3) = b3 ) ) )

reconsider j9 = j as Element of MSAlg_set (S,A) by Def4;
consider MS being strict feasible MSAlgebra over S such that
A38: MS = j9 and
for C being Component of the Sorts of MS holds C c= A by Def2;
reconsider e = id the Sorts of MS as ManySortedFunction of MS,MS ;
take e ; :: thesis: ( e in the Arrows of (MSAlgCat (S,A)) . (j,j) & ( for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 ) ) )

( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (j,j) = MSAlg_morph (S,A,j9,j9) ) by ;
hence A39: e in the Arrows of (MSAlgCat (S,A)) . (j,j) by ; :: thesis: for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (b1,j) or ( the Comp of (MSAlgCat (S,A)) . (b1,j,j)) . (e,b2) = b2 )

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

reconsider i9 = i as Element of MSAlg_set (S,A) by Def4;
let f be set ; :: thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f )
reconsider I = i, J = j as Object of (MSAlgCat (S,A)) ;
assume A40: f in the Arrows of (MSAlgCat (S,A)) . (i,j) ; :: thesis: ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f
then f in MSAlg_morph (S,A,i9,j9) by Def4;
then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that
M1 = i9 and
A41: N1 = j9 and
A42: F = f and
the Sorts of M1 is_transformable_to the Sorts of N1 and
F is_homomorphism M1,N1 by Def3;
reconsider F = F as ManySortedFunction of M1,MS by ;
( the Comp of (MSAlgCat (S,A)) . (I,J,J)) . (e,f) = e ** F by ;
hence ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f by ; :: thesis: verum
end;
thus the Comp of (MSAlgCat (S,A)) is with_right_units :: thesis: verum
proof
let i be Element of (MSAlgCat (S,A)); :: according to ALTCAT_1:def 6 :: thesis: ex b1 being set st
( b1 in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b2 being Element of the carrier of (MSAlgCat (S,A))
for b3 being set holds
( not b3 in the Arrows of (MSAlgCat (S,A)) . (i,b2) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b2)) . (b3,b1) = b3 ) ) )

reconsider i9 = i as Element of MSAlg_set (S,A) by Def4;
consider MS being strict feasible MSAlgebra over S such that
A43: MS = i9 and
for C being Component of the Sorts of MS holds C c= A by Def2;
reconsider e = id the Sorts of MS as ManySortedFunction of MS,MS ;
take e ; :: thesis: ( e in the Arrows of (MSAlgCat (S,A)) . (i,i) & ( for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 ) ) )

( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (i,i) = MSAlg_morph (S,A,i9,i9) ) by ;
hence A44: e in the Arrows of (MSAlgCat (S,A)) . (i,i) by ; :: thesis: for b1 being Element of the carrier of (MSAlgCat (S,A))
for b2 being set holds
( not b2 in the Arrows of (MSAlgCat (S,A)) . (i,b1) or ( the Comp of (MSAlgCat (S,A)) . (i,i,b1)) . (b2,e) = b2 )

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

reconsider j9 = j as Element of MSAlg_set (S,A) by Def4;
let f be set ; :: thesis: ( not f in the Arrows of (MSAlgCat (S,A)) . (i,j) or ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f )
reconsider I = i, J = j as Object of (MSAlgCat (S,A)) ;
assume A45: f in the Arrows of (MSAlgCat (S,A)) . (i,j) ; :: thesis: ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f
then f in MSAlg_morph (S,A,i9,j9) by Def4;
then consider M1, N1 being strict feasible MSAlgebra over S, F being ManySortedFunction of M1,N1 such that
A46: M1 = i9 and
N1 = j9 and
A47: F = f and
the Sorts of M1 is_transformable_to the Sorts of N1 and
F is_homomorphism M1,N1 by Def3;
reconsider F = F as ManySortedFunction of MS,N1 by ;
( the Comp of (MSAlgCat (S,A)) . (I,I,J)) . (f,e) = F ** e by ;
hence ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f by ; :: thesis: verum
end;