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

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

now

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

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 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 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 6;
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 6;
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:23;
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:9;
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:9; :: 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:10; :: thesis: verum