reconsider c = MSAlg_set (S,A) as non empty set ;
let A1, A2 be non empty strict AltCatStr ; :: thesis: ( the carrier of A1 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of A1 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( 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 ) & the carrier of A2 = MSAlg_set (S,A) & ( for i, j being Element of MSAlg_set (S,A) holds the Arrows of A2 . (i,j) = MSAlg_morph (S,A,i,j) ) & ( 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 ) implies A1 = A2 )

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: A1 = A2
reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:c,c,c:] by ;
reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet of [:c,c:] by ;
A31: now :: thesis: for i, j being Element of c holds AA1 . (i,j) = AA2 . (i,j)
let i, j be Element of c; :: thesis: AA1 . (i,j) = AA2 . (i,j)
thus AA1 . (i,j) = MSAlg_morph (S,A,i,j) by A26
.= AA2 . (i,j) by A29 ; :: thesis: verum
end;
then A32: AA1 = AA2 by ALTCAT_1:7;
now :: thesis: for i, j, k being object st i in c & j in c & k in c holds
CC1 . (i,j,k) = CC2 . (i,j,k)
let i, j, k be object ; :: thesis: ( i in c & j in c & k in c implies CC1 . (i,j,k) = CC2 . (i,j,k) )
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: CC1 . (i,j,k) = CC2 . (i,j,k)
then reconsider i9 = i, j9 = j, k9 = k as Element of c ;
reconsider I9 = i, J9 = j, K9 = k as Object of A2 by ;
reconsider I = i, J = j, K = k as Object of A1 by ;
A35: [i,j,k] in [:c,c,c:] by ;
A36: CC2 . (i,j,k) = CC2 . [i,j,k] by MULTOP_1:def 1;
thus CC1 . (i,j,k) = CC2 . (i,j,k) :: thesis: verum
proof
reconsider Cj = CC2 . [i,j,k] as Function of ({|AA2,AA2|} . [i,j,k]),({|AA2|} . [i,j,k]) by ;
reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by ;
per cases ( {|AA1|} . [i,j,k] <> {} or {|AA1|} . [i,j,k] = {} ) ;
suppose A37: {|AA1|} . [i,j,k] <> {} ; :: thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
A38: for x being object st x in {|AA1,AA1|} . [i,j,k] holds
Ci . x = Cj . x
proof
let x be object ; :: thesis: ( x in {|AA1,AA1|} . [i,j,k] implies Ci . x = Cj . x )
assume A39: x in {|AA1,AA1|} . [i,j,k] ; :: thesis: Ci . x = Cj . x
then x in {|AA1,AA1|} . (i,j,k) by MULTOP_1:def 1;
then A40: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by ;
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 ;
then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by ;
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 ;
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 ;
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 ;
hence Ci . x = Cj . x ; :: thesis: verum
end;
{|AA2|} . [i,j,k] <> {} by ;
then A47: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def 1;
dom Ci = {|AA1,AA1|} . [i,j,k] by ;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by ; :: thesis: verum
end;
suppose {|AA1|} . [i,j,k] = {} ; :: thesis: CC1 . (i,j,k) = CC2 . (i,j,k)
then ( Ci = {} & Cj = {} ) by A32;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by ; :: thesis: verum
end;
end;
end;
end;
hence A1 = A2 by ; :: thesis: verum