let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty Circuit of IIG
for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of () . v st v in SortsWithConstants IIG holds
(() . v) . e = root-tree [(), the carrier of IIG]

let A be non-empty Circuit of IIG; :: thesis: for iv being InputValues of A
for v being Vertex of IIG
for e being Element of the Sorts of () . v st v in SortsWithConstants IIG holds
(() . v) . e = root-tree [(), the carrier of IIG]

let iv be InputValues of A; :: thesis: for v being Vertex of IIG
for e being Element of the Sorts of () . v st v in SortsWithConstants IIG holds
(() . v) . e = root-tree [(), the carrier of IIG]

let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of () . v st v in SortsWithConstants IIG holds
(() . v) . e = root-tree [(), the carrier of IIG]

let e be Element of the Sorts of () . v; :: thesis: ( v in SortsWithConstants IIG implies (() . v) . e = root-tree [(), the carrier of IIG] )
set X = the Sorts of A;
assume A1: v in SortsWithConstants IIG ; :: thesis: (() . v) . e = root-tree [(), the carrier of IIG]
A2: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;
then e in (FreeSort the Sorts of A) . v ;
then e in FreeSort ( the Sorts of A,v) by MSAFREE:def 11;
then e in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) )
}
by MSAFREE:def 10;
then A3: ex a being Element of TS (DTConMSA the Sorts of A) st
( e = a & ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) ) ;
per cases ( ex x being set st
( x in the Sorts of A . v & e = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = e . {} & the_result_sort_of o = v ) )
by A3;
suppose A4: ex x being set st
( x in the Sorts of A . v & e = root-tree [x,v] ) ; :: thesis: (() . v) . e = root-tree [(), the carrier of IIG]
Fix_inp iv c= Fix_inp_ext iv by Def2;
then A5: (Fix_inp iv) . v c= () . v ;
A6: e in FreeGen (v, the Sorts of A) by ;
then e in (FreeGen the Sorts of A) . v by MSAFREE:def 16;
then e in dom ((Fix_inp iv) . v) by FUNCT_2:def 1;
hence (() . v) . e = ((Fix_inp iv) . v) . e by
.= ((FreeGen (v, the Sorts of A)) --> (root-tree [(), the carrier of IIG])) . e by
.= root-tree [(), the carrier of IIG] by ;
:: thesis: verum
end;
suppose ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = e . {} & the_result_sort_of o = v ) ; :: thesis: (() . v) . e = root-tree [(), the carrier of IIG]
then consider o9 being OperSymbol of IIG such that
A7: [o9, the carrier of IIG] = e . {} and
A8: the_result_sort_of o9 = v ;
A9: SortsWithConstants IIG c= InnerVertices IIG by MSAFREE2:3;
then o9 = action_at v by ;
then consider q being DTree-yielding FinSequence such that
A10: e = [(), the carrier of IIG] -tree q by ;
v in { s where s is SortSymbol of IIG : s is with_const_op } by ;
then ex s being SortSymbol of IIG st
( v = s & s is with_const_op ) ;
then consider o being OperSymbol of IIG such that
A11: the Arity of IIG . o = {} and
A12: the ResultSort of IIG . o = v by MSUALG_2:def 1;
A13: Fix_inp_ext iv is_homomorphism FreeEnv A, FreeEnv A by Def2;
the_result_sort_of o = v by ;
then A14: o = action_at v by ;
action_at v in the carrier' of IIG ;
then A15: action_at v in dom the Arity of IIG by FUNCT_2:def 1;
A16: Args ((),()) = (( the Sorts of () #) * the Arity of IIG) . () by MSUALG_1:def 4
.= ( the Sorts of () #) . (<*> the carrier of IIG) by
.= by PRE_CIRC:2 ;
then reconsider x = {} as Element of Args ((),()) by TARSKI:def 1;
A17: x = () # x by ;
A18: Args ((),()) = (((FreeSort the Sorts of A) #) * the Arity of IIG) . o by ;
then reconsider p = x as FinSequence of TS (DTConMSA the Sorts of A) by MSAFREE:8;
A19: Sym ((), the Sorts of A) ==> roots p by ;
A20: the_result_sort_of () = v by ;
then len q = len () by
.= len {} by
.= 0 ;
then q = {} ;
then A21: e = root-tree [(), the carrier of IIG] by ;
(Den ((),())) . x = ((FreeOper the Sorts of A) . ()) . x by
.= (DenOp ((), the Sorts of A)) . x by MSAFREE:def 13
.= (Sym ((), the Sorts of A)) -tree p by
.= [(), the carrier of IIG] -tree p by MSAFREE:def 9
.= root-tree [(), the carrier of IIG] by TREES_4:20 ;
hence ((Fix_inp_ext iv) . v) . e = root-tree [(), the carrier of IIG] by ; :: thesis: verum
end;
end;