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 for i being object st i in SortsWithConstants IIG holds
it1 . i = it2 . ilet i be
object ;
( 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 3;
dom it2 = SortsWithConstants IIG
by PARTFUN1:def 2;
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 2;
dom it1 = SortsWithConstants IIG
by PARTFUN1:def 2;
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
object st
(
x2 in dom (Den (o2,SCS)) &
a2 = (Den (o2,SCS)) . x2 )
by A18, FUNCT_1:def 3;
the_result_sort_of o1 = v
by A23, MSUALG_1:def 2;
then A27:
o1 = o2
by A19, MSAFREE2:def 6;
consider x1 being
object such that A28:
x1 in dom (Den (o1,SCS))
and A29:
a1 = (Den (o1,SCS)) . x1
by A24, FUNCT_1:def 3;
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 4
.=
( the Sorts of SCS #) . ( the Arity of IIG . o1)
by A12, FUNCT_1:13
.=
{{}}
by A22, A25, PRE_CIRC:2
;
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