set c = MSS_set A;

let A1, A2 be non empty strict AltCatStr ; :: thesis: ( the carrier of A1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of A1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds

( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of A2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of A2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds

( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) implies A1 = A2 )

assume that

A23: the carrier of A1 = MSS_set A and

A24: for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) and

A25: for i, j, k being Object of A1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds

( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] and

A26: the carrier of A2 = MSS_set A and

A27: for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) and

A28: for i, j, k being Object of A2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds

( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ; :: thesis: A1 = A2

reconsider AA2 = the Arrows of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A26;

reconsider AA1 = the Arrows of A1 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A23;

reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A),(MSS_set A):] by A23, A26;

let A1, A2 be non empty strict AltCatStr ; :: thesis: ( the carrier of A1 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of A1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds

( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) & the carrier of A2 = MSS_set A & ( for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) ) & ( for i, j, k being Object of A2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds

( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ) implies A1 = A2 )

assume that

A23: the carrier of A1 = MSS_set A and

A24: for i, j being Element of MSS_set A holds the Arrows of A1 . (i,j) = MSS_morph (i,j) and

A25: for i, j, k being Object of A1 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A1 . (i,j) & [g1,g2] in the Arrows of A1 . (j,k) holds

( the Comp of A1 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] and

A26: the carrier of A2 = MSS_set A and

A27: for i, j being Element of MSS_set A holds the Arrows of A2 . (i,j) = MSS_morph (i,j) and

A28: for i, j, k being Object of A2 st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

for f1, f2, g1, g2 being Function st [f1,f2] in the Arrows of A2 . (i,j) & [g1,g2] in the Arrows of A2 . (j,k) holds

( the Comp of A2 . (i,j,k)) . ([g1,g2],[f1,f2]) = [(g1 * f1),(g2 * f2)] ; :: thesis: A1 = A2

reconsider AA2 = the Arrows of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A26;

reconsider AA1 = the Arrows of A1 as ManySortedSet of [:(MSS_set A),(MSS_set A):] by A23;

reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:(MSS_set A),(MSS_set A),(MSS_set A):] by A23, A26;

A29: now :: thesis: for i, j being Element of MSS_set A holds AA1 . (i,j) = AA2 . (i,j)

then A30:
AA1 = AA2
by ALTCAT_1:7;let i, j be Element of MSS_set A; :: thesis: AA1 . (i,j) = AA2 . (i,j)

thus AA1 . (i,j) = MSS_morph (i,j) by A24

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

end;thus AA1 . (i,j) = MSS_morph (i,j) by A24

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

now :: thesis: for i, j, k being object st i in MSS_set A & j in MSS_set A & k in MSS_set A holds

CC1 . (i,j,k) = CC2 . (i,j,k)

hence
A1 = A2
by A23, A26, A30, ALTCAT_1:8; :: thesis: verumCC1 . (i,j,k) = CC2 . (i,j,k)

let i, j, k be object ; :: thesis: ( i in MSS_set A & j in MSS_set A & k in MSS_set A implies CC1 . (i,j,k) = CC2 . (i,j,k) )

set ijk = [i,j,k];

A31: CC1 . (i,j,k) = CC1 . [i,j,k] by MULTOP_1:def 1;

assume A32: ( i in MSS_set A & j in MSS_set A & k in MSS_set A ) ; :: thesis: CC1 . (i,j,k) = CC2 . (i,j,k)

then reconsider i9 = i, j9 = j, k9 = k as Element of MSS_set A ;

reconsider I9 = i, J9 = j, K9 = k as Element of A2 by A26, A32;

reconsider I = i, J = j, K = k as Element of A1 by A23, A32;

A33: [i,j,k] in [:(MSS_set A),(MSS_set A),(MSS_set A):] by A32, MCART_1:69;

A34: 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];

A31: CC1 . (i,j,k) = CC1 . [i,j,k] by MULTOP_1:def 1;

assume A32: ( i in MSS_set A & j in MSS_set A & k in MSS_set A ) ; :: thesis: CC1 . (i,j,k) = CC2 . (i,j,k)

then reconsider i9 = i, j9 = j, k9 = k as Element of MSS_set A ;

reconsider I9 = i, J9 = j, K9 = k as Element of A2 by A26, A32;

reconsider I = i, J = j, K = k as Element of A1 by A23, A32;

A33: [i,j,k] in [:(MSS_set A),(MSS_set A),(MSS_set A):] by A32, MCART_1:69;

A34: 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 A26, A33, PBOOLE:def 15;

reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A23, A33, PBOOLE:def 15;

end;reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by A23, A33, PBOOLE:def 15;

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

end;

suppose A35:
{|AA1|} . [i,j,k] <> {}
; :: thesis: CC1 . (i,j,k) = CC2 . (i,j,k)

A36:
for x being object st x in {|AA1,AA1|} . [i,j,k] holds

Ci . x = Cj . x

then A45: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def 1;

dom Ci = {|AA1,AA1|} . [i,j,k] by A35, FUNCT_2:def 1;

hence CC1 . (i,j,k) = CC2 . (i,j,k) by A30, A31, A34, A45, A36, FUNCT_1:2; :: thesis: verum

end;Ci . x = Cj . x

proof

{|AA2|} . [i,j,k] <> {}
by A29, A35, ALTCAT_1:7;
let x be object ; :: thesis: ( x in {|AA1,AA1|} . [i,j,k] implies Ci . x = Cj . x )

assume A37: 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 A38: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by A32, ALTCAT_1:def 4;

then A39: x `1 in AA1 . (j,k) by MCART_1:10;

then x `1 in MSS_morph (j9,k9) by A24;

then consider g1, g2 being Function such that

A40: x `1 = [g1,g2] and

g1,g2 form_morphism_between j9,k9 by MSALIMIT:def 10;

x in {|AA2,AA2|} . (i,j,k) by A30, A37, MULTOP_1:def 1;

then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by A32, ALTCAT_1:def 4;

then A41: ( x `1 in AA2 . (j,k) & x `2 in AA2 . (i,j) ) by MCART_1:10;

A42: x `2 in AA1 . (i,j) by A38, MCART_1:10;

then x `2 in MSS_morph (i9,j9) by A24;

then consider f1, f2 being Function such that

A43: x `2 = [f1,f2] and

f1,f2 form_morphism_between i9,j9 by MSALIMIT:def 10;

A44: x = [[g1,g2],[f1,f2]] by A38, A40, A43, MCART_1:21;

then Ci . x = ( the Comp of A1 . (I,J,K)) . ([g1,g2],[f1,f2]) by MULTOP_1:def 1

.= [(g1 * f1),(g2 * f2)] by A23, A25, A39, A42, A40, A43

.= ( the Comp of A2 . (I9,J9,K9)) . ([g1,g2],[f1,f2]) by A26, A28, A41, A40, A43

.= Cj . x by A44, MULTOP_1:def 1 ;

hence Ci . x = Cj . x ; :: thesis: verum

end;assume A37: 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 A38: x in [:(AA1 . (j,k)),(AA1 . (i,j)):] by A32, ALTCAT_1:def 4;

then A39: x `1 in AA1 . (j,k) by MCART_1:10;

then x `1 in MSS_morph (j9,k9) by A24;

then consider g1, g2 being Function such that

A40: x `1 = [g1,g2] and

g1,g2 form_morphism_between j9,k9 by MSALIMIT:def 10;

x in {|AA2,AA2|} . (i,j,k) by A30, A37, MULTOP_1:def 1;

then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by A32, ALTCAT_1:def 4;

then A41: ( x `1 in AA2 . (j,k) & x `2 in AA2 . (i,j) ) by MCART_1:10;

A42: x `2 in AA1 . (i,j) by A38, MCART_1:10;

then x `2 in MSS_morph (i9,j9) by A24;

then consider f1, f2 being Function such that

A43: x `2 = [f1,f2] and

f1,f2 form_morphism_between i9,j9 by MSALIMIT:def 10;

A44: x = [[g1,g2],[f1,f2]] by A38, A40, A43, MCART_1:21;

then Ci . x = ( the Comp of A1 . (I,J,K)) . ([g1,g2],[f1,f2]) by MULTOP_1:def 1

.= [(g1 * f1),(g2 * f2)] by A23, A25, A39, A42, A40, A43

.= ( the Comp of A2 . (I9,J9,K9)) . ([g1,g2],[f1,f2]) by A26, A28, A41, A40, A43

.= Cj . x by A44, MULTOP_1:def 1 ;

hence Ci . x = Cj . x ; :: thesis: verum

then A45: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def 1;

dom Ci = {|AA1,AA1|} . [i,j,k] by A35, FUNCT_2:def 1;

hence CC1 . (i,j,k) = CC2 . (i,j,k) by A30, A31, A34, A45, A36, FUNCT_1:2; :: thesis: verum