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