set c = MSAlg_set S,A;
deffunc H₁( 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₁(i,j) from ALTCAT_1:sch 2();
defpred S₁[ set , set , set ] 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 set st ijk in [:(MSAlg_set S,A),(MSAlg_set S,A),(MSAlg_set S,A):] holds
for x being set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S₁[y,x,ijk] )

proof

let ijk be set ; :: thesis: ( ijk in [:(MSAlg_set S,A),(MSAlg_set S,A),(MSAlg_set S,A):] implies for x being set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S₁[y,x,ijk] ) )
assume ijk in [:(MSAlg_set S,A),(MSAlg_set S,A),(MSAlg_set S,A):] ; :: thesis: for x being set st x in {|M,M|} . ijk holds
ex y being set st
( y in {|M|} . ijk & S₁[y,x,ijk] )
then consider x1, x2, x3 being set 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:72;
reconsider x1 = x1, x2 = x2, x3 = x3 as Element of MSAlg_set S,A by A3;
let x be set ; :: thesis: ( x in {|M,M|} . ijk implies ex y being set st
( y in {|M|} . ijk & S₁[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 6, 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 set st
( y in {|M|} . ijk & S₁[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 of 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 of 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₁[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:11;
then ( {|M|} . x1,x2,x3 = M . x1,x3 & y in MSAlg_morph S,A,x1,x3 ) by A9, A12, Def3, ALTCAT_1:def 5;
hence y in {|M|} . ijk by A1, A6; :: thesis: S₁[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
x `1 = G by A16, MCART_1:7;
hence y = G ** F by A10, A14, A16, MCART_1:7; :: thesis: verum

end;

consider F being ManySortedFunction of {|M,M|},{|M|} such that
A17: for ijk being set 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 set st x in {|M,M|} . ijk holds
S₁[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

proof

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:73;
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 set st x in {|M,M|} . [i,j,k] holds
S₁[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 6, MULTOP_1:def 1;
then [g,f] in {|M,M|} . [i,j,k] by A18, ZFMISC_1:106;
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, MCART_1:28;
( I = i & J = j ) by A22, MCART_1:28;
hence (the Comp of EX . i,j,k) . g,f = g ** f by A18, A23, A24, A21; :: thesis: verum

end;

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
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