let IIG be non empty non void Circuit-like ManySortedSign ; for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e
let SCS be non-empty Circuit of IIG; for v being Vertex of IIG
for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e
let v be Vertex of IIG; for e being Element of the Sorts of SCS . v st v in SortsWithConstants IIG & e in Constants (SCS,v) holds
(Set-Constants SCS) . v = e
let e be Element of the Sorts of SCS . v; ( v in SortsWithConstants IIG & e in Constants (SCS,v) implies (Set-Constants SCS) . v = e )
assume that
A1:
v in SortsWithConstants IIG
and
A2:
e in Constants (SCS,v)
; (Set-Constants SCS) . v = e
A3:
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;
then
ex a being Element of the Sorts of SCS . v st
( a = e & 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 A2;
then consider o being OperSymbol of IIG such that
A4:
the Arity of IIG . o = {}
and
A5:
the ResultSort of IIG . o = v
and
A6:
e in rng (Den (o,SCS))
;
A7:
{} = <*> the carrier of IIG
;
v in dom (Set-Constants SCS)
by A1, PARTFUN1:def 2;
then
(Set-Constants SCS) . v in Constants (SCS,v)
by Def1;
then
ex a being Element of the Sorts of SCS . v st
( a = (Set-Constants SCS) . v & 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 A3;
then consider o1 being OperSymbol of IIG such that
the Arity of IIG . o1 = {}
and
A8:
the ResultSort of IIG . o1 = v
and
A9:
(Set-Constants SCS) . v in rng (Den (o1,SCS))
;
A10:
ex d1 being object st
( d1 in dom (Den (o1,SCS)) & (Set-Constants SCS) . v = (Den (o1,SCS)) . d1 )
by A9, FUNCT_1:def 3;
( the_result_sort_of o = the ResultSort of IIG . o & the_result_sort_of o1 = the ResultSort of IIG . o1 )
by MSUALG_1:def 2;
then A11:
o = o1
by A5, A8, MSAFREE2:def 6;
consider d being object such that
A12:
d in dom (Den (o,SCS))
and
A13:
e = (Den (o,SCS)) . d
by A6, FUNCT_1:def 3;
A14:
dom the Arity of IIG = the carrier' of IIG
by FUNCT_2:def 1;
A15: dom (Den (o,SCS)) =
Args (o,SCS)
by FUNCT_2:def 1
.=
(( the Sorts of SCS #) * the Arity of IIG) . o
by MSUALG_1:def 4
.=
( the Sorts of SCS #) . ( the Arity of IIG . o)
by A14, FUNCT_1:13
.=
{{}}
by A4, A7, PRE_CIRC:2
;
then
d = {}
by A12, TARSKI:def 1;
hence
(Set-Constants SCS) . v = e
by A11, A15, A13, A10, TARSKI:def 1; verum