reconsider c = MSAlg_set S,A as non empty set ;
let A1, A2 be non empty strict AltCatStr ; :: thesis:
assume that
A19: ( 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 ) ) and
A20: ( 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 ) ) ; :: thesis:
reconsider AA1 = the Arrows of A1, AA2 = the Arrows of A2 as ManySortedSet of by A19, A20;

A21: now

let i, j be Element of c; :: thesis:
thus AA1 . i,j = MSAlg_morph S,A,i,j by A19
.= AA2 . i,j by A20 ; :: thesis:

end;

then A22: AA1 = AA2 by ALTCAT_1:9;
reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of by A19, A20;

now

let i, j, k be set ; :: thesis:
assume A23: ( i in c & j in c & k in c ) ; :: thesis:
then reconsider i' = i, j' = j, k' = k as Element of c ;
reconsider I = i, J = j, K = k as object of A1 by A19, A23;
reconsider I' = i, J' = j, K' = k as object of A2 by A20, A23;
set ijk = [i,j,k];
A24: ( CC1 . i,j,k = CC1 . [i,j,k] & CC2 . i,j,k = CC2 . [i,j,k] ) by MULTOP_1:def 1;
A25: [i,j,k] in [:c,c,c:] by A23, MCART_1:73;
thus CC1 . i,j,k = CC2 . i,j,k :: thesis:

proof

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

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

suppose A26: {|AA1|} . [i,j,k] <> {} ; :: thesis:

then {|AA2|} . [i,j,k] <> {} by A21, ALTCAT_1:9;
then A27: ( dom Ci = {|AA1,AA1|} . [i,j,k] & dom Cj = {|AA2,AA2|} . [i,j,k] ) by A26, FUNCT_2:def 1;
for x being set st x in {|AA1,AA1|} . [i,j,k] holds
Ci . x = Cj . x

proof

let x be set ; :: thesis:
assume x in {|AA1,AA1|} . [i,j,k] ; :: thesis:
then ( x in {|AA1,AA1|} . i,j,k & x in {|AA2,AA2|} . i,j,k ) by A22, MULTOP_1:def 1;
then A28: ( x in [:(AA1 . j,k),(AA1 . i,j):] & x in [:(AA2 . j,k),(AA2 . i,j):] ) by A23, ALTCAT_1:def 6;
then A29: ( x `1 in AA1 . j,k & x `2 in AA1 . i,j & x `1 in AA2 . j,k & x `2 in AA2 . i,j ) by MCART_1:10;
then A30: ( x `1 in MSAlg_morph S,A,j',k' & x `2 in MSAlg_morph S,A,i',j' ) by A19;
then consider M1, N1 being strict feasible MSAlgebra of S, f being ManySortedFunction of M1,N1 such that
A31: ( M1 = i' & N1 = j' & f = x `2 & the Sorts of M1 is_transformable_to the Sorts of N1 & f is_homomorphism M1,N1 ) by Def3;
consider M2, N2 being strict feasible MSAlgebra of S, g being ManySortedFunction of M2,N2 such that
A32: ( M2 = j' & N2 = k' & g = x `1 & the Sorts of M2 is_transformable_to the Sorts of N2 & g is_homomorphism M2,N2 ) by A30, Def3;
A33: x = [g,f] by A28, A31, A32, MCART_1:23;
then Ci . x = (the Comp of A1 . I,J,K) . g,f by MULTOP_1:def 1
.= g ** f by A19, A29, A31, A32
.= (the Comp of A2 . I',J',K') . g,f by A20, A29, A31, A32
.= Cj . x by A33, MULTOP_1:def 1 ;
hence Ci . x = Cj . x ; :: thesis:

end;

hence CC1 . i,j,k = CC2 . i,j,k by A22, A24, A27, FUNCT_1:9; :: thesis:

end;

suppose {|AA1|} . [i,j,k] = {} ; :: thesis:

then ( rng Ci = {} & rng Cj = {} ) by A22;
then ( Ci = {} & Cj = {} ) ;
hence CC1 . i,j,k = CC2 . i,j,k by A24; :: thesis:

end;

hence A1 = A2 by A19, A20, A22, ALTCAT_1:10; :: thesis: