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 [:(),():] by A26;
reconsider AA1 = the Arrows of A1 as ManySortedSet of [:(),():] by A23;
reconsider CC1 = the Comp of A1, CC2 = the Comp of A2 as ManySortedSet of [:(),(),():] by ;
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 ;
reconsider I = i, J = j, K = k as Element of A1 by ;
A33: [i,j,k] in [:(),(),():] by ;
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 ;
reconsider Ci = CC1 . [i,j,k] as Function of ({|AA1,AA1|} . [i,j,k]),({|AA1|} . [i,j,k]) by ;
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 ;
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 ;
then x in [:(AA2 . (j,k)),(AA2 . (i,j)):] by ;
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 ;
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 ;
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 ;
hence Ci . x = Cj . x ; :: thesis: verum
end;
{|AA2|} . [i,j,k] <> {} by ;
then A45: dom Cj = {|AA2,AA2|} . [i,j,k] by FUNCT_2:def 1;
dom Ci = {|AA1,AA1|} . [i,j,k] by ;
hence CC1 . (i,j,k) = CC2 . (i,j,k) by ; :: 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 ; :: thesis: verum
end;
end;
end;
end;
hence A1 = A2 by ; :: thesis: verum