reconsider c = MSAlg_set (S,A) as non empty set ;
let A1, A2 be non empty strict AltCatStr ; :: thesis:
assume that
A25: the carrier of A1 = MSAlg_set (S,A) and
A26: for i, j being Element of MSAlg_set (S,A) holds the Arrows of A1 . (i,j) = MSAlg_morph (S,A,i,j) and
A27: for i, j, k being Object of A1
for f, g being Function-yielding Function st f in the Arrows of A1 . (i,j) & g in the Arrows of A1 . (j,k) holds
( the Comp of A1 . (i,j,k)) . (g,f) = g ** f and
A28: the carrier of A2 = MSAlg_set (S,A) and
A29: for i, j being Element of MSAlg_set (S,A) holds the Arrows of A2 . (i,j) = MSAlg_morph (S,A,i,j) and
A30: for i, j, k being Object of A2
for f, g being Function-yielding Function st f in the Arrows of A2 . (i,j) & g in the Arrows of A2 . (j,k) holds
( the Comp of A2 . (i,j,k)) . (g,f) = g ** f ; :: thesis:
reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:c,c,c:] by A25, A28;
reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet of [:c,c:] by A25, A28;

let i, j be Element of c; :: thesis:
thus AA1 . (i,j) = MSAlg_morph (S,A,i,j) by A26
.= AA2 . (i,j) by A29 ; :: thesis:

end;

let i, j, k be object ; :: thesis:
set ijk = [i,j,k];
A33: CC1 . (i,j,k) = CC1 . [i,j,k] by MULTOP_1:def 1;
assume A34: ( i in c & j in c & k in c ) ; :: thesis:
then reconsider i9 = i, j9 = j, k9 = k as Element of c ;
reconsider I9 = i, J9 = j, K9 = k as Object of A2 by A28, A34;
reconsider I = i, J = j, K = k as Object of A1 by A25, A34;
A35: [i,j,k] in [:c,c,c:] by A34, MCART_1:69;
A36: CC2 . (i,j,k) = CC2 . [i,j,k] by MULTOP_1:def 1;
thus CC1 . (i,j,k) = CC2 . (i,j,k) :: thesis:

reconsider Cj = CC2 . [i,j,k] as Function of ({|AA2,AA2|} . [i,j,k]),({|AA2|} . [i,j,k]) by A28, A35, PBOOLE:def 15;
reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A25, A35, PBOOLE:def 15;

per cases . [i,j,k] <> {} or {|AA1|} . [i,j,k] = {} ) ;

A38: for x being object st x in {|AA1,AA1|} . [i,j,k] holds
Ci . x = Cj . x

let x be object ; :: thesis:
assume A39: x in {|AA1,AA1|} . [i,j,k] ; :: thesis:
then x in {|AA1,AA1|} . (i,j,k) by MULTOP_1:def 1;
then A40: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by A34, ALTCAT_1:def 4;
then A41: x `1 in AA1 . (j,k) by MCART_1:10;
then x `1 in MSAlg_morph (S,A,j9,k9) by A26;
then consider M2, N2 being strict feasible MSAlgebra over S, g being ManySortedFunction of M2,N2 such that
M2 = j9 and
N2 = k9 and
A42: g = x `1 and
the Sorts of M2 is_transformable_to the Sorts of N2 and
g is_homomorphism M2,N2 by Def3;
x in {|AA2,AA2|} . (i,j,k) by A32, A39, MULTOP_1:def 1;
then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by A34, ALTCAT_1:def 4;
then A43: ( x `1 in AA2 . (j,k) & x `2 in AA2 . (i,j) ) by MCART_1:10;
A44: x `2 in AA1 . (i,j) by A40, MCART_1:10;
then x `2 in MSAlg_morph (S,A,i9,j9) by A26;
then consider M1, N1 being strict feasible MSAlgebra over S, f being ManySortedFunction of M1,N1 such that
M1 = i9 and
N1 = j9 and
A45: f = x `2 and
the Sorts of M1 is_transformable_to the Sorts of N1 and
f is_homomorphism M1,N1 by Def3;
A46: x = [g,f] by A40, A45, A42, MCART_1:21;
then Ci . x = ( the Comp of A1 . (I,J,K)) . (g,f) by MULTOP_1:def 1
.= g ** f by A27, A41, A44, A45, A42
.= ( the Comp of A2 . (I9,J9,K9)) . (g,f) by A30, A43, A45, A42
.= Cj . x by A46, MULTOP_1:def 1 ;
hence Ci . x = Cj . x ; :: thesis:

end;

end;

then ( Ci = {} & Cj = {} ) by A32;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by A33, MULTOP_1:def 1; :: thesis:

end;