let S be non void Signature; :: thesis: for X, Y being ManySortedSet of
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 ; :: 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 X = the carrier of S & dom Y = the carrier of S )
by PARTFUN1:def 4;
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 A0:
( g1 = g2 & p1 = p2 & g1 ==> p1 )
; :: thesis: g2 ==> p2
then Y4:
[g1,p1] in REL X
by LANG1:def 1;
then Y5:
( g1 in [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) & p1 in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * )
by ZFMISC_1:106;
then Y6:
g1 in [:the carrier' of S,{the carrier of S}:]
by Y4, MSAFREE:def 9;
Y9:
p2 in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod Y))) *
by FINSEQ_1:def 11;
now let o' be
OperSymbol of
S;
:: thesis: ( [o',the carrier of S] = g2 implies ( len p2 = len (the_arity_of o') & ( 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 o') . x ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod ((the_arity_of o') . x),Y ) ) ) ) )assume Y7:
[o',the carrier of S] = g2
;
:: thesis: ( len p2 = len (the_arity_of o') & ( 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 o') . x ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod ((the_arity_of o') . x),Y ) ) ) )hence Z4:
len p2 = len (the_arity_of o')
by A0, Y4, Y5, MSAFREE:def 9;
:: 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 o') . x ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod ((the_arity_of o') . 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 o') . x ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod ((the_arity_of o') . x),Y ) ) )assume Y8:
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 o') . x ) & ( p2 . x in Union (coprod Y) implies p2 . x in coprod ((the_arity_of o') . 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 o') . x )
by A0, Y4, Y5, Y7, MSAFREE:def 9;
:: thesis: ( p2 . x in Union (coprod Y) implies p2 . x in coprod ((the_arity_of o') . x),Y )
x in dom (the_arity_of o')
by Z4, Y8, FINSEQ_3:31;
then
(the_arity_of o') . x in rng (the_arity_of o')
by FUNCT_1:def 5;
then reconsider i =
(the_arity_of o') . x as
SortSymbol of
S ;
assume
p2 . x in Union (coprod Y)
;
:: thesis: p2 . x in coprod ((the_arity_of o') . x),Ythen B1:
(
(p2 . x) `2 in dom Y &
(p2 . x) `1 in Y . ((p2 . x) `2 ) &
p2 . x = [((p2 . x) `1 ),((p2 . x) `2 )] )
by CARD_3:33;
p2 . x in rng p1
by A0, Y8, FUNCT_1:def 5;
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;
then
p2 . x in coprod i,
X
by A0, Y4, Y5, Y7, Y8, A1, B1, MSAFREE:def 9, ZFMISC_1:129;
then consider a being
set such that Z3:
(
a in X . i &
p2 . x = [a,i] )
by MSAFREE:def 2;
i = (p2 . x) `2
by B1, Z3, ZFMISC_1:33;
hence
p2 . x in coprod ((the_arity_of o') . x),
Y
by B1, MSAFREE:def 2;
:: thesis: verum end;
then
[g2,p2] in REL Y
by A0, Y6, Y9, MSAFREE:def 9;
hence
g2 ==> p2
by LANG1:def 1; :: thesis: verum