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