let it1, it2 be ManySortedSet of SortsWithConstants IIG; ( ( for x being Vertex of IIG st x in dom it1 holds
it1 . x in Constants SCS,x ) & ( for x being Vertex of IIG st x in dom it2 holds
it2 . x in Constants SCS,x ) implies it1 = it2 )
assume A10:
for x being Vertex of IIG st x in dom it1 holds
it1 . x in Constants SCS,x
; ( ex x being Vertex of IIG st
( x in dom it2 & not it2 . x in Constants SCS,x ) or it1 = it2 )
assume A11:
for x being Vertex of IIG st x in dom it2 holds
it2 . x in Constants SCS,x
; it1 = it2
now let i be
set ;
( i in SortsWithConstants IIG implies it1 . i = it2 . i )A12:
dom the
Arity of
IIG = the
carrier' of
IIG
by FUNCT_2:def 1;
assume A13:
i in SortsWithConstants IIG
;
it1 . i = it2 . ithen reconsider v =
i as
Vertex of
IIG ;
A14:
ex
A being non
empty set st
(
A = the
Sorts of
SCS . v &
Constants SCS,
v = { a where a is Element of A : ex o being OperSymbol of IIG st
( the Arity of IIG . o = {} & the ResultSort of IIG . o = v & a in rng (Den o,SCS) ) } )
by MSUALG_2:def 4;
dom it2 = SortsWithConstants IIG
by PARTFUN1:def 4;
then
it2 . v in Constants SCS,
v
by A11, A13;
then consider a2 being
Element of the
Sorts of
SCS . v such that A15:
it2 . v = a2
and A16:
ex
o being
OperSymbol of
IIG st
( the
Arity of
IIG . o = {} & the
ResultSort of
IIG . o = v &
a2 in rng (Den o,SCS) )
by A14;
consider o2 being
OperSymbol of
IIG such that
the
Arity of
IIG . o2 = {}
and A17:
the
ResultSort of
IIG . o2 = v
and A18:
a2 in rng (Den o2,SCS)
by A16;
A19:
the_result_sort_of o2 = v
by A17, MSUALG_1:def 7;
dom it1 = SortsWithConstants IIG
by PARTFUN1:def 4;
then
it1 . v in Constants SCS,
v
by A10, A13;
then consider a1 being
Element of the
Sorts of
SCS . v such that A20:
it1 . v = a1
and A21:
ex
o being
OperSymbol of
IIG st
( the
Arity of
IIG . o = {} & the
ResultSort of
IIG . o = v &
a1 in rng (Den o,SCS) )
by A14;
consider o1 being
OperSymbol of
IIG such that A22:
the
Arity of
IIG . o1 = {}
and A23:
the
ResultSort of
IIG . o1 = v
and A24:
a1 in rng (Den o1,SCS)
by A21;
A25:
{} = <*> the
carrier of
IIG
;
A26:
ex
x2 being
set st
(
x2 in dom (Den o2,SCS) &
a2 = (Den o2,SCS) . x2 )
by A18, FUNCT_1:def 5;
the_result_sort_of o1 = v
by A23, MSUALG_1:def 7;
then A27:
o1 = o2
by A19, MSAFREE2:def 6;
consider x1 being
set such that A28:
x1 in dom (Den o1,SCS)
and A29:
a1 = (Den o1,SCS) . x1
by A24, FUNCT_1:def 5;
A30:
dom (Den o1,SCS) =
Args o1,
SCS
by FUNCT_2:def 1
.=
((the Sorts of SCS # ) * the Arity of IIG) . o1
by MSUALG_1:def 9
.=
(the Sorts of SCS # ) . (the Arity of IIG . o1)
by A12, FUNCT_1:23
.=
{{} }
by A22, A25, PRE_CIRC:5
;
then
x1 = {}
by A28, TARSKI:def 1;
hence
it1 . i = it2 . i
by A20, A15, A27, A30, A29, A26, TARSKI:def 1;
verum end;
hence
it1 = it2
by PBOOLE:3; verum