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 (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), 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 (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), 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 (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v st v in SortsWithConstants IIG holds
((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]
let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: ( v in SortsWithConstants IIG implies ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG] )
set X = the Sorts of A;
assume A1: v in SortsWithConstants IIG ; :: thesis: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), 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: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG]

Fix_inp iv c= Fix_inp_ext iv by Def2;
then A5: (Fix_inp iv) . v c= (Fix_inp_ext iv) . v ;
A6: e in FreeGen (v, the Sorts of A) by A4, MSAFREE:def 15;
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 ((Fix_inp_ext iv) . v) . e = ((Fix_inp iv) . v) . e by A5, GRFUNC_1:2
.= ((FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG])) . e by A1, Def1
.= root-tree [(action_at v), the carrier of IIG] by A6, FUNCOP_1:7 ;
:: thesis: verum

end;

suppose ex o being OperSymbol of IIG st
( [o, the carrier of IIG] = e . {} & the_result_sort_of o = v ) ; :: thesis: ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), 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 A1, A8, MSAFREE2:def 7;
then consider q being DTree-yielding FinSequence such that
A10: e = [(action_at v), the carrier of IIG] -tree q by A7, CIRCUIT1:9;
v in { s where s is SortSymbol of IIG : s is with_const_op } by A1, MSAFREE2:def 1;
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 A12, MSUALG_1:def 2;
then A14: o = action_at v by A1, A9, MSAFREE2:def 7;
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 ((action_at v),(FreeEnv A)) = (( the Sorts of (FreeEnv A) #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4
.= ( the Sorts of (FreeEnv A) #) . (<*> the carrier of IIG) by A11, A14, A15, FUNCT_1:13
.= {{}} by PRE_CIRC:2 ;
then reconsider x = {} as Element of Args ((action_at v),(FreeEnv A)) by TARSKI:def 1;
A17: x = (Fix_inp_ext iv) # x by A16, TARSKI:def 1;
A18: Args ((action_at v),(FreeEnv A)) = (((FreeSort the Sorts of A) #) * the Arity of IIG) . o by A2, A14, MSUALG_1:def 4;
then reconsider p = x as FinSequence of TS (DTConMSA the Sorts of A) by MSAFREE:8;
A19: Sym ((action_at v), the Sorts of A) ==> roots p by A14, A18, MSAFREE:10;
A20: the_result_sort_of (action_at v) = v by A1, A9, MSAFREE2:def 7;
then len q = len (the_arity_of (action_at v)) by A10, MSAFREE2:10
.= len {} by A11, A14, MSUALG_1:def 1
.= 0 ;
then q = {} ;
then A21: e = root-tree [(action_at v), the carrier of IIG] by A10, TREES_4:20;
(Den ((action_at v),(FreeEnv A))) . x = ((FreeOper the Sorts of A) . (action_at v)) . x by A2, MSUALG_1:def 6
.= (DenOp ((action_at v), the Sorts of A)) . x by MSAFREE:def 13
.= (Sym ((action_at v), the Sorts of A)) -tree p by A19, MSAFREE:def 12
.= [(action_at v), the carrier of IIG] -tree p by MSAFREE:def 9
.= root-tree [(action_at v), the carrier of IIG] by TREES_4:20 ;
hence ((Fix_inp_ext iv) . v) . e = root-tree [(action_at v), the carrier of IIG] by A20, A17, A13, A21, MSUALG_3:def 7; :: thesis: verum

end;

end;