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 A25, A28;
reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet of [:c,c:] by A25, A28;

A31: now

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:9;

now

let i, j, k be set ; :: 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 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:73;
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 A28, A35, PBOOLE:def 18;
reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A25, A35, PBOOLE:def 18;

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 set st x in {|AA1,AA1|} . [i,j,k] holds
Ci . x = Cj . x

proof

let x be set ; :: 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 A34, ALTCAT_1:def 6;
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 of 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 6;
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 of 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:23;
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: verum

end;

{|AA2|} . [i,j,k] <> {} by A31, A37, ALTCAT_1:9;
then A47: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def 1;
dom Ci = {|AA1,AA1|} . [i,j,k] by A37, FUNCT_2:def 1;
hence CC1 . i,j,k = CC2 . i,j,k by A32, A33, A36, A47, A38, FUNCT_1:9; :: 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 A33, MULTOP_1:def 1; :: thesis: verum

end;

end;

end;

end;

hence A1 = A2 by A25, A28, A32, ALTCAT_1:10; :: thesis: verum