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;

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 :: thesis: for i, j being Element of c holds AA1 . (i,j) = AA2 . (i,j)

then A32:
AA1 = AA2
by ALTCAT_1:7;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;thus AA1 . (i,j) = MSAlg_morph (S,A,i,j) by A26

.= AA2 . (i,j) by A29 ; :: thesis: verum

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)

hence
A1 = A2
by A25, A28, A32, ALTCAT_1:8; :: thesis: verumCC1 . (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 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: verum

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

end;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
( {|AA1|} . [i,j,k] <> {} or {|AA1|} . [i,j,k] = {} )
;

end;

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

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:2; :: thesis: verum

end;Ci . x = Cj . x

proof

{|AA2|} . [i,j,k] <> {}
by A31, A37, ALTCAT_1:7;
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 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: verum

end;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 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: verum

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:2; :: thesis: verum