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;

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

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;

then A30: AA1 = AA2 by ALTCAT_1:7;

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)

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

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;

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

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

proof

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;

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

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

then ( Ci = {} & Cj = {} ) by A30;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by A31, MULTOP_1:def 1; :: thesis: verum

end;

end;

end;

end;

hence A1 = A2 by A23, A26, A30, ALTCAT_1:8; :: thesis: verum