set c = MSAlg_set (S,A);

deffunc H_{1}( Element of MSAlg_set (S,A), Element of MSAlg_set (S,A)) -> set = MSAlg_morph (S,A,$1,$2);

consider M being ManySortedSet of [:(MSAlg_set (S,A)),(MSAlg_set (S,A)):] such that

A1: for i, j being Element of MSAlg_set (S,A) holds M . (i,j) = H_{1}(i,j)
from ALTCAT_1:sch 2();

defpred S_{1}[ object , object , object ] means ex i, j, k being Element of MSAlg_set (S,A) st

( $3 = [i,j,k] & ( for f, g being Function-yielding Function st f in M . (i,j) & g in M . (j,k) & $2 = [g,f] holds

$1 = g ** f ) );

A2: for ijk being object st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds

for x being object st x in {|M,M|} . ijk holds

ex y being object st

( y in {|M|} . ijk & S_{1}[y,x,ijk] )

A17: for ijk being object st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds

ex f being Function of ({|M,M|} . ijk),({|M|} . ijk) st

( f = F . ijk & ( for x being object st x in {|M,M|} . ijk holds

S_{1}[f . x,x,ijk] ) )
from MSSUBFAM:sch 1(A2);

take EX = AltCatStr(# (MSAlg_set (S,A)),M,F #); :: thesis: ( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of EX

for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds

( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) )

reconsider EX = EX as non empty AltCatStr ;

for i, j, k being Object of EX

for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds

( the Comp of EX . (i,j,k)) . (g,f) = g ** f

for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds

( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) ) by A1; :: thesis: verum

deffunc H

consider M being ManySortedSet of [:(MSAlg_set (S,A)),(MSAlg_set (S,A)):] such that

A1: for i, j being Element of MSAlg_set (S,A) holds M . (i,j) = H

defpred S

( $3 = [i,j,k] & ( for f, g being Function-yielding Function st f in M . (i,j) & g in M . (j,k) & $2 = [g,f] holds

$1 = g ** f ) );

A2: for ijk being object st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds

for x being object st x in {|M,M|} . ijk holds

ex y being object st

( y in {|M|} . ijk & S

proof

consider F being ManySortedFunction of {|M,M|},{|M|} such that
let ijk be object ; :: thesis: ( ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] implies for x being object st x in {|M,M|} . ijk holds

ex y being object st

( y in {|M|} . ijk & S_{1}[y,x,ijk] ) )

assume ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] ; :: thesis: for x being object st x in {|M,M|} . ijk holds

ex y being object st

( y in {|M|} . ijk & S_{1}[y,x,ijk] )

then consider x1, x2, x3 being object such that

A3: ( x1 in MSAlg_set (S,A) & x2 in MSAlg_set (S,A) & x3 in MSAlg_set (S,A) ) and

A4: ijk = [x1,x2,x3] by MCART_1:68;

reconsider x1 = x1, x2 = x2, x3 = x3 as Element of MSAlg_set (S,A) by A3;

let x be object ; :: thesis: ( x in {|M,M|} . ijk implies ex y being object st

( y in {|M|} . ijk & S_{1}[y,x,ijk] ) )

A5: ( {|M,M|} . (x1,x2,x3) = {|M,M|} . [x1,x2,x3] & {|M,M|} . (x1,x2,x3) = [:(M . (x2,x3)),(M . (x1,x2)):] ) by ALTCAT_1:def 4, MULTOP_1:def 1;

A6: {|M|} . ijk = {|M|} . (x1,x2,x3) by A4, MULTOP_1:def 1;

assume A7: x in {|M,M|} . ijk ; :: thesis: ex y being object st

( y in {|M|} . ijk & S_{1}[y,x,ijk] )

then x `1 in M . (x2,x3) by A4, A5, MCART_1:10;

then x `1 in MSAlg_morph (S,A,x2,x3) by A1;

then consider M2, N2 being strict feasible MSAlgebra over S, g being ManySortedFunction of M2,N2 such that

A8: M2 = x2 and

A9: N2 = x3 and

A10: g = x `1 and

A11: ( the Sorts of M2 is_transformable_to the Sorts of N2 & g is_homomorphism M2,N2 ) by Def3;

x `2 in M . (x1,x2) by A4, A7, A5, MCART_1:10;

then x `2 in MSAlg_morph (S,A,x1,x2) by A1;

then consider M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that

A12: M1 = x1 and

A13: N1 = x2 and

A14: f = x `2 and

A15: ( the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) by Def3;

take y = g ** f; :: thesis: ( y in {|M|} . ijk & S_{1}[y,x,ijk] )

reconsider f = f as ManySortedFunction of M1,M2 by A8, A13;

( the Sorts of M1 is_transformable_to the Sorts of N2 & ex fg being ManySortedFunction of M1,N2 st

( fg = g ** f & fg is_homomorphism M1,N2 ) ) by A8, A11, A13, A15, Th5, AUTALG_1:10;

then ( {|M|} . (x1,x2,x3) = M . (x1,x3) & y in MSAlg_morph (S,A,x1,x3) ) by A9, A12, Def3, ALTCAT_1:def 3;

hence y in {|M|} . ijk by A1, A6; :: thesis: S_{1}[y,x,ijk]

take x1 ; :: thesis: ex j, k being Element of MSAlg_set (S,A) st

( ijk = [x1,j,k] & ( for f, g being Function-yielding Function st f in M . (x1,j) & g in M . (j,k) & x = [g,f] holds

y = g ** f ) )

take x2 ; :: thesis: ex k being Element of MSAlg_set (S,A) st

( ijk = [x1,x2,k] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,k) & x = [g,f] holds

y = g ** f ) )

take x3 ; :: thesis: ( ijk = [x1,x2,x3] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds

y = g ** f ) )

thus ijk = [x1,x2,x3] by A4; :: thesis: for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds

y = g ** f

let F, G be Function-yielding Function; :: thesis: ( F in M . (x1,x2) & G in M . (x2,x3) & x = [G,F] implies y = G ** F )

assume that

F in M . (x1,x2) and

G in M . (x2,x3) and

A16: x = [G,F] ; :: thesis: y = G ** F

thus y = G ** F by A10, A14, A16; :: thesis: verum

end;ex y being object st

( y in {|M|} . ijk & S

assume ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] ; :: thesis: for x being object st x in {|M,M|} . ijk holds

ex y being object st

( y in {|M|} . ijk & S

then consider x1, x2, x3 being object such that

A3: ( x1 in MSAlg_set (S,A) & x2 in MSAlg_set (S,A) & x3 in MSAlg_set (S,A) ) and

A4: ijk = [x1,x2,x3] by MCART_1:68;

reconsider x1 = x1, x2 = x2, x3 = x3 as Element of MSAlg_set (S,A) by A3;

let x be object ; :: thesis: ( x in {|M,M|} . ijk implies ex y being object st

( y in {|M|} . ijk & S

A5: ( {|M,M|} . (x1,x2,x3) = {|M,M|} . [x1,x2,x3] & {|M,M|} . (x1,x2,x3) = [:(M . (x2,x3)),(M . (x1,x2)):] ) by ALTCAT_1:def 4, MULTOP_1:def 1;

A6: {|M|} . ijk = {|M|} . (x1,x2,x3) by A4, MULTOP_1:def 1;

assume A7: x in {|M,M|} . ijk ; :: thesis: ex y being object st

( y in {|M|} . ijk & S

then x `1 in M . (x2,x3) by A4, A5, MCART_1:10;

then x `1 in MSAlg_morph (S,A,x2,x3) by A1;

then consider M2, N2 being strict feasible MSAlgebra over S, g being ManySortedFunction of M2,N2 such that

A8: M2 = x2 and

A9: N2 = x3 and

A10: g = x `1 and

A11: ( the Sorts of M2 is_transformable_to the Sorts of N2 & g is_homomorphism M2,N2 ) by Def3;

x `2 in M . (x1,x2) by A4, A7, A5, MCART_1:10;

then x `2 in MSAlg_morph (S,A,x1,x2) by A1;

then consider M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that

A12: M1 = x1 and

A13: N1 = x2 and

A14: f = x `2 and

A15: ( the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) by Def3;

take y = g ** f; :: thesis: ( y in {|M|} . ijk & S

reconsider f = f as ManySortedFunction of M1,M2 by A8, A13;

( the Sorts of M1 is_transformable_to the Sorts of N2 & ex fg being ManySortedFunction of M1,N2 st

( fg = g ** f & fg is_homomorphism M1,N2 ) ) by A8, A11, A13, A15, Th5, AUTALG_1:10;

then ( {|M|} . (x1,x2,x3) = M . (x1,x3) & y in MSAlg_morph (S,A,x1,x3) ) by A9, A12, Def3, ALTCAT_1:def 3;

hence y in {|M|} . ijk by A1, A6; :: thesis: S

take x1 ; :: thesis: ex j, k being Element of MSAlg_set (S,A) st

( ijk = [x1,j,k] & ( for f, g being Function-yielding Function st f in M . (x1,j) & g in M . (j,k) & x = [g,f] holds

y = g ** f ) )

take x2 ; :: thesis: ex k being Element of MSAlg_set (S,A) st

( ijk = [x1,x2,k] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,k) & x = [g,f] holds

y = g ** f ) )

take x3 ; :: thesis: ( ijk = [x1,x2,x3] & ( for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds

y = g ** f ) )

thus ijk = [x1,x2,x3] by A4; :: thesis: for f, g being Function-yielding Function st f in M . (x1,x2) & g in M . (x2,x3) & x = [g,f] holds

y = g ** f

let F, G be Function-yielding Function; :: thesis: ( F in M . (x1,x2) & G in M . (x2,x3) & x = [G,F] implies y = G ** F )

assume that

F in M . (x1,x2) and

G in M . (x2,x3) and

A16: x = [G,F] ; :: thesis: y = G ** F

thus y = G ** F by A10, A14, A16; :: thesis: verum

A17: for ijk being object st ijk in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] holds

ex f being Function of ({|M,M|} . ijk),({|M|} . ijk) st

( f = F . ijk & ( for x being object st x in {|M,M|} . ijk holds

S

take EX = AltCatStr(# (MSAlg_set (S,A)),M,F #); :: thesis: ( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of EX

for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds

( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) )

reconsider EX = EX as non empty AltCatStr ;

for i, j, k being Object of EX

for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds

( the Comp of EX . (i,j,k)) . (g,f) = g ** f

proof

hence
( the carrier of EX = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of EX . (i,j) = MSAlg_morph (S,A,i,j) ) & ( for i, j, k being Object of EX
let i, j, k be Object of EX; :: thesis: for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds

( the Comp of EX . (i,j,k)) . (g,f) = g ** f

let f, g be Function-yielding Function; :: thesis: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) implies ( the Comp of EX . (i,j,k)) . (g,f) = g ** f )

assume A18: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) ) ; :: thesis: ( the Comp of EX . (i,j,k)) . (g,f) = g ** f

set x = [g,f];

set ijk = [i,j,k];

[i,j,k] in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] by MCART_1:69;

then consider ff being Function of ({|M,M|} . [i,j,k]),({|M|} . [i,j,k]) such that

A19: ff = F . [i,j,k] and

A20: for x being object st x in {|M,M|} . [i,j,k] holds

S_{1}[ff . x,x,[i,j,k]]
by A17;

A21: ff = the Comp of EX . (i,j,k) by A19, MULTOP_1:def 1;

( {|M,M|} . (i,j,k) = {|M,M|} . [i,j,k] & {|M,M|} . (i,j,k) = [:(M . (j,k)),(M . (i,j)):] ) by ALTCAT_1:def 4, MULTOP_1:def 1;

then [g,f] in {|M,M|} . [i,j,k] by A18, ZFMISC_1:87;

then consider I, J, K being Element of MSAlg_set (S,A) such that

A22: [i,j,k] = [I,J,K] and

A23: for f, g being Function-yielding Function st f in M . (I,J) & g in M . (J,K) & [g,f] = [g,f] holds

ff . [g,f] = g ** f by A20;

A24: K = k by A22, XTUPLE_0:3;

( I = i & J = j ) by A22, XTUPLE_0:3;

hence ( the Comp of EX . (i,j,k)) . (g,f) = g ** f by A18, A23, A24, A21; :: thesis: verum

end;( the Comp of EX . (i,j,k)) . (g,f) = g ** f

let f, g be Function-yielding Function; :: thesis: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) implies ( the Comp of EX . (i,j,k)) . (g,f) = g ** f )

assume A18: ( f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) ) ; :: thesis: ( the Comp of EX . (i,j,k)) . (g,f) = g ** f

set x = [g,f];

set ijk = [i,j,k];

[i,j,k] in [:(MSAlg_set (S,A)),(MSAlg_set (S,A)),(MSAlg_set (S,A)):] by MCART_1:69;

then consider ff being Function of ({|M,M|} . [i,j,k]),({|M|} . [i,j,k]) such that

A19: ff = F . [i,j,k] and

A20: for x being object st x in {|M,M|} . [i,j,k] holds

S

A21: ff = the Comp of EX . (i,j,k) by A19, MULTOP_1:def 1;

( {|M,M|} . (i,j,k) = {|M,M|} . [i,j,k] & {|M,M|} . (i,j,k) = [:(M . (j,k)),(M . (i,j)):] ) by ALTCAT_1:def 4, MULTOP_1:def 1;

then [g,f] in {|M,M|} . [i,j,k] by A18, ZFMISC_1:87;

then consider I, J, K being Element of MSAlg_set (S,A) such that

A22: [i,j,k] = [I,J,K] and

A23: for f, g being Function-yielding Function st f in M . (I,J) & g in M . (J,K) & [g,f] = [g,f] holds

ff . [g,f] = g ** f by A20;

A24: K = k by A22, XTUPLE_0:3;

( I = i & J = j ) by A22, XTUPLE_0:3;

hence ( the Comp of EX . (i,j,k)) . (g,f) = g ** f by A18, A23, A24, A21; :: thesis: verum

for f, g being Function-yielding Function st f in the Arrows of EX . (i,j) & g in the Arrows of EX . (j,k) holds

( the Comp of EX . (i,j,k)) . (g,f) = g ** f ) ) by A1; :: thesis: verum