let S be non void Signature; :: thesis:
let X, Y be ManySortedSet of the carrier of S; :: thesis:
A1: dom Y = the carrier of S by PARTFUN1:def 2;
set G1 = DTConMSA X;
set G2 = DTConMSA Y;
let g1 be Symbol of (DTConMSA X); :: thesis:
let g2 be Symbol of (DTConMSA Y); :: thesis:
let p1 be FinSequence of the carrier of (DTConMSA X); :: thesis:
let p2 be FinSequence of the carrier of (DTConMSA Y); :: thesis:
assume that
A2: g1 = g2 and
A3: p1 = p2 and
A4: g1 ==> p1 ; :: thesis:
A5: [g1,p1] in REL X by A4;
then A6: p1 in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by ZFMISC_1:87;
then A7: g1 in [: the carrier' of S,{ the carrier of S}:] by A5, MSAFREE:def 7;
A8: p2 in ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod Y))) * by FINSEQ_1:def 11;

let o9 be OperSymbol of S; :: thesis:
assume A9: [o9, the carrier of S] = g2 ; :: thesis:
hence A10: len p2 = len (the_arity_of o9) by A2, A3, A5, A6, MSAFREE:def 7; :: thesis:
let x be set ; :: thesis:
assume A11: x in dom p2 ; :: thesis:
hence ( p2 . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = p2 . x holds
the_result_sort_of o1 = (the_arity_of o9) . x ) by A2, A3, A5, A6, A9, MSAFREE:def 7; :: thesis:
x in dom (the_arity_of o9) by A10, A11, FINSEQ_3:29;
then (the_arity_of o9) . x in rng (the_arity_of o9) by FUNCT_1:def 3;
then reconsider i = (the_arity_of o9) . x as SortSymbol of S ;
assume A12: p2 . x in Union (coprod Y) ; :: thesis:
then A13: (p2 . x) `2 in dom Y by CARD_3:22;
A14: (p2 . x) `1 in Y . ((p2 . x) `2) by A12, CARD_3:22;
A15: p2 . x = [((p2 . x) `1),((p2 . x) `2)] by A12, CARD_3:22;
reconsider nn = the carrier of S as set ;
A: not nn in nn ;
p2 . x in rng p1 by A3, A11, FUNCT_1:def 3;
then ( ( the carrier of S nin the carrier of S & p2 . x in [: the carrier' of S,{ the carrier of S}:] ) or p2 . x in Union (coprod X) ) by XBOOLE_0:def 3, A;
then p2 . x in coprod (i,X) by A1, A2, A3, A5, A6, A9, A11, A13, A15, MSAFREE:def 7, ZFMISC_1:106;
then ex a being set st
( a in X . i & p2 . x = [a,i] ) by MSAFREE:def 2;
then i = (p2 . x) `2 ;
hence p2 . x in coprod (((the_arity_of o9) . x),Y) by A14, A15, MSAFREE:def 2; :: thesis:

end;

then [g2,p2] in REL Y by A2, A7, A8, MSAFREE:def 7;
hence g2 ==> p2 ; :: thesis: