let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG
for v being Vertex of IIG
for iv being InputValues of SCS st v in SortsWithConstants IIG holds
IGValue (v,iv) = () . v

reconsider p = {} as DTree-yielding FinSequence ;
let SCS be non-empty Circuit of IIG; :: thesis: for v being Vertex of IIG
for iv being InputValues of SCS st v in SortsWithConstants IIG holds
IGValue (v,iv) = () . v

let v be Vertex of IIG; :: thesis: for iv being InputValues of SCS st v in SortsWithConstants IIG holds
IGValue (v,iv) = () . v

let iv be InputValues of SCS; :: thesis: ( v in SortsWithConstants IIG implies IGValue (v,iv) = () . v )
assume A1: v in SortsWithConstants IIG ; :: thesis: IGValue (v,iv) = () . v
set e = ((Eval SCS) . v) . (root-tree [(), the carrier of IIG]);
A2: {} = <*> the carrier of IIG ;
set X = the Sorts of SCS;
set F = Eval SCS;
A3: dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
A4: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
set o = action_at v;
A5: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
then A6: v = the_result_sort_of () by ;
SortsWithConstants IIG = { v1 where v1 is SortSymbol of IIG : v1 is with_const_op } by MSAFREE2:def 1;
then consider x9 being SortSymbol of IIG such that
A7: x9 = v and
A8: x9 is with_const_op by A1;
consider o1 being OperSymbol of IIG such that
A9: the Arity of IIG . o1 = {} and
A10: the ResultSort of IIG . o1 = x9 by ;
the ResultSort of IIG . o1 = the_result_sort_of o1 by MSUALG_1:def 2;
then A11: action_at v = o1 by ;
A12: Args ((),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . () by MSUALG_1:def 4
.= ( the Sorts of (FreeEnv SCS) #) . ( the Arity of IIG . ()) by
.= by ;
then reconsider x = {} as Element of Args ((),(FreeEnv SCS)) by TARSKI:def 1;
reconsider Fx = (Eval SCS) # x as Element of Args ((),SCS) ;
Eval SCS is_homomorphism FreeEnv SCS,SCS by MSAFREE2:def 9;
then A13: ((Eval SCS) . ()) . ((Den ((),(FreeEnv SCS))) . x) = (Den ((),SCS)) . Fx by MSUALG_3:def 7;
A14: FreeMSA the Sorts of SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 14;
then A15: Den ((),(FreeEnv SCS)) = (FreeOper the Sorts of SCS) . () by MSUALG_1:def 6
.= DenOp ((), the Sorts of SCS) by MSAFREE:def 13 ;
{} in Args ((),(FreeEnv SCS)) by ;
then A16: p in (((FreeSort the Sorts of SCS) #) * the Arity of IIG) . () by ;
then reconsider p9 = {} as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;
Sym ((), the Sorts of SCS) ==> roots p9 by ;
then A17: (Den ((),(FreeEnv SCS))) . {} = (Sym ((), the Sorts of SCS)) -tree p by
.= [(), the carrier of IIG] -tree {} by MSAFREE:def 9
.= root-tree [(), the carrier of IIG] by TREES_4:20 ;
dom (Den ((),SCS)) = Args ((),SCS) by FUNCT_2:def 1;
then A18: ((Eval SCS) . v) . (root-tree [(), the carrier of IIG]) in rng (Den ((),SCS)) by ;
Result ((),SCS) = ( the Sorts of SCS * the ResultSort of IIG) . () by MSUALG_1:def 5
.= the Sorts of SCS . ( the ResultSort of IIG . ()) by ;
then reconsider e = ((Eval SCS) . v) . (root-tree [(), the carrier of IIG]) as Element of the Sorts of SCS . v by ;
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 A19: e in Constants (SCS,v) by A7, A9, A10, A11, A18;
ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & IGTree (v,iv) = (() . v) . e ) by Def3;
hence IGValue (v,iv) = e by
.= () . v by ;
:: thesis: verum