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 )

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

thus
the Comp of (MSAlgCat (S,A)) is associative
:: according to ALTCAT_1:def 15 :: thesis: MSAlgCat (S,A) is with_units
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 A1, Def4;

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 A2, Def4;

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 A4, A5, A7, A9, AUTALG_1:10;

then GF in MSAlg_morph (S,A,o19,o39) by A3, A8, A11, Def3;

hence not <^o1,o3^> = {} by Def4; :: thesis: verum

end;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 A1, Def4;

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 A2, Def4;

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 A4, A5, A7, A9, AUTALG_1:10;

then GF in MSAlg_morph (S,A,o19,o39) by A3, A8, A11, Def3;

hence not <^o1,o3^> = {} by Def4; :: thesis: verum

proof

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
let i, j, k, l be Element of (MSAlgCat (S,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 (MSAlgCat (S,A)) . (i,j) or not b_{2} in the Arrows of (MSAlgCat (S,A)) . (j,k) or not b_{3} in the Arrows of (MSAlgCat (S,A)) . (k,l) or ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (b_{3},(( the Comp of (MSAlgCat (S,A)) . (i,j,k)) . (b_{2},b_{1}))) = ( the Comp of (MSAlgCat (S,A)) . (i,j,l)) . ((( the Comp of (MSAlgCat (S,A)) . (j,k,l)) . (b_{3},b_{2})),b_{1}) )

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 A13, Def4;

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 A14, Def4;

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 A16, A20;

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 A12, Def4;

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 A29, A31, A15, A16, A18, A20, AUTALG_1:10;

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 A34, Def4;

then A36: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (H,GF) = H ** GF by A14, A22, Def4;

the Sorts of M2 is_transformable_to the Sorts of N3 by A16, A18, A20, A23, AUTALG_1:10;

then HG in MSAlg_morph (S,A,j9,l9) by A15, A21, A26, Def3;

then A37: H ** G9 in the Arrows of (MSAlgCat (S,A)) . (j,l) by A25, Def4;

(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;( not b

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 A13, Def4;

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 A14, Def4;

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 A16, A20;

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 A12, Def4;

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 A29, A31, A15, A16, A18, A20, AUTALG_1:10;

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 A34, Def4;

then A36: ( the Comp of (MSAlgCat (S,A)) . (i,k,l)) . (H,GF) = H ** GF by A14, A22, Def4;

the Sorts of M2 is_transformable_to the Sorts of N3 by A16, A18, A20, A23, AUTALG_1:10;

then HG in MSAlg_morph (S,A,j9,l9) by A15, A21, A26, Def3;

then A37: H ** G9 in the Arrows of (MSAlgCat (S,A)) . (j,l) by A25, Def4;

(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

proof

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

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

for b_{3} being set holds

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

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 b_{1} being Element of the carrier of (MSAlgCat (S,A))

for b_{2} being set holds

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

( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (j,j) = MSAlg_morph (S,A,j9,j9) ) by Def4, MSUALG_3:9;

hence A39: e in the Arrows of (MSAlgCat (S,A)) . (j,j) by A38, Def3; :: thesis: for b_{1} being Element of the carrier of (MSAlgCat (S,A))

for b_{2} being set holds

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

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

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

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 A38, A41;

( the Comp of (MSAlgCat (S,A)) . (I,J,J)) . (e,f) = e ** F by A39, A40, A42, Def4;

hence ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f by A42, MSUALG_3:4; :: thesis: verum

end;( b

for b

( not b

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 b

for b

( not b

( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (j,j) = MSAlg_morph (S,A,j9,j9) ) by Def4, MSUALG_3:9;

hence A39: e in the Arrows of (MSAlgCat (S,A)) . (j,j) by A38, Def3; :: thesis: for b

for b

( not b

let i be Element of (MSAlgCat (S,A)); :: thesis: for b

( not b

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 A38, A41;

( the Comp of (MSAlgCat (S,A)) . (I,J,J)) . (e,f) = e ** F by A39, A40, A42, Def4;

hence ( the Comp of (MSAlgCat (S,A)) . (i,j,j)) . (e,f) = f by A42, MSUALG_3:4; :: thesis: verum

proof

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

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

for b_{3} being set holds

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

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 b_{1} being Element of the carrier of (MSAlgCat (S,A))

for b_{2} being set holds

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

( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (i,i) = MSAlg_morph (S,A,i9,i9) ) by Def4, MSUALG_3:9;

hence A44: e in the Arrows of (MSAlgCat (S,A)) . (i,i) by A43, Def3; :: thesis: for b_{1} being Element of the carrier of (MSAlgCat (S,A))

for b_{2} being set holds

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

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

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

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 A43, A46;

( the Comp of (MSAlgCat (S,A)) . (I,I,J)) . (f,e) = F ** e by A44, A45, A47, Def4;

hence ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f by A47, MSUALG_3:3; :: thesis: verum

end;( b

for b

( not b

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 b

for b

( not b

( e is_homomorphism MS,MS & the Arrows of (MSAlgCat (S,A)) . (i,i) = MSAlg_morph (S,A,i9,i9) ) by Def4, MSUALG_3:9;

hence A44: e in the Arrows of (MSAlgCat (S,A)) . (i,i) by A43, Def3; :: thesis: for b

for b

( not b

let j be Element of (MSAlgCat (S,A)); :: thesis: for b

( not b

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 A43, A46;

( the Comp of (MSAlgCat (S,A)) . (I,I,J)) . (f,e) = F ** e by A44, A45, A47, Def4;

hence ( the Comp of (MSAlgCat (S,A)) . (i,i,j)) . (f,e) = f by A47, MSUALG_3:3; :: thesis: verum