let S be non void Signature; :: thesis: for X, Y being ManySortedSet of the carrier of S
for g1 being Symbol of (DTConMSA X)
for g2 being Symbol of (DTConMSA Y)
for p1 being FinSequence of the carrier of (DTConMSA X)
for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds
g2 ==> p2
let X, Y be ManySortedSet of the carrier of S; :: thesis: for g1 being Symbol of (DTConMSA X)
for g2 being Symbol of (DTConMSA Y)
for p1 being FinSequence of the carrier of (DTConMSA X)
for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds
g2 ==> p2
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: for g2 being Symbol of (DTConMSA Y)
for p1 being FinSequence of the carrier of (DTConMSA X)
for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds
g2 ==> p2
let g2 be Symbol of (DTConMSA Y); :: thesis: for p1 being FinSequence of the carrier of (DTConMSA X)
for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds
g2 ==> p2
let p1 be FinSequence of the carrier of (DTConMSA X); :: thesis: for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds
g2 ==> p2
let p2 be FinSequence of the carrier of (DTConMSA Y); :: thesis: ( g1 = g2 & p1 = p2 & g1 ==> p1 implies g2 ==> p2 )
assume that
A2: g1 = g2 and
A3: p1 = p2 and
A4: g1 ==> p1 ; :: thesis: g2 ==> p2
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;

now :: thesis: for o9 being OperSymbol of S st [o9, the carrier of S] = g2 holds
( len p2 = len (the_arity_of o9) & ( for x being set st x in dom p2 holds
( ( 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 ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod (((the_arity_of o9) . x),Y) ) ) ) )

let o9 be OperSymbol of S; :: thesis: ( [o9, the carrier of S] = g2 implies ( len p2 = len (the_arity_of o9) & ( for x being set st x in dom p2 holds
( ( 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 ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod (((the_arity_of o9) . x),Y) ) ) ) ) )
assume A9: [o9, the carrier of S] = g2 ; :: thesis: ( len p2 = len (the_arity_of o9) & ( for x being set st x in dom p2 holds
( ( 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 ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod (((the_arity_of o9) . x),Y) ) ) ) )
hence A10: len p2 = len (the_arity_of o9) by A2, A3, A5, A6, MSAFREE:def 7; :: thesis: for x being set st x in dom p2 holds
( ( 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 ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod (((the_arity_of o9) . x),Y) ) )
let x be set ; :: thesis: ( x in dom p2 implies ( ( 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 ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod (((the_arity_of o9) . x),Y) ) ) )
assume A11: x in dom p2 ; :: thesis: ( ( 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 ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod (((the_arity_of o9) . x),Y) ) )
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: ( p2 . x in Union (coprod Y) implies p2 . x in coprod (((the_arity_of o9) . x),Y) )
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: p2 . x in coprod (((the_arity_of o9) . x),Y)
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: verum

end;

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