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₁[ 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₁[y,x,ijk] )

proof

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₁[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₁[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₁[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₁[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₁[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₁[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;

consider F being ManySortedFunction of {|M,M|},{|M|} such that
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₁[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: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₁[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;

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