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
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = (() . (() /. k)) . (p . k) ) holds
(() . v) . e = [(), the carrier of IIG] -tree q

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
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = (() . (() /. k)) . (p . k) ) holds
(() . v) . e = [(), the carrier of IIG] -tree q

let iv be InputValues of A; :: thesis: for v being Vertex of IIG
for e being Element of the Sorts of () . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = (() . (() /. k)) . (p . k) ) holds
(() . v) . e = [(), the carrier of IIG] -tree q

let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of () . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = (() . (() /. k)) . (p . k) ) holds
(() . v) . e = [(), the carrier of IIG] -tree q

let e be Element of the Sorts of () . v; :: thesis: for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = (() . (() /. k)) . (p . k) ) holds
(() . v) . e = [(), the carrier of IIG] -tree q

let p, q be DTree-yielding FinSequence; :: thesis: ( v in InnerVertices IIG & e = [(), the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = (() . (() /. k)) . (p . k) ) implies (() . v) . e = [(), the carrier of IIG] -tree q )

assume that
A1: v in InnerVertices IIG and
A2: e = [(), the carrier of IIG] -tree p and
A3: dom p = dom q and
A4: for k being Element of NAT st k in dom p holds
q . k = (() . (() /. k)) . (p . k) ; :: thesis: (() . v) . e = [(), the carrier of IIG] -tree q
set o = action_at v;
A5: the_result_sort_of () = v by ;
then A6: len p = len () by ;
A7: now :: thesis: for k being Nat st k in dom q holds
q . k in the Sorts of () . (() /. k)
let k be Nat; :: thesis: ( k in dom q implies q . k in the Sorts of () . (() /. k) )
assume A8: k in dom q ; :: thesis: q . k in the Sorts of () . (() /. k)
then A9: k in dom () by ;
then p . k in the Sorts of () . (() . k) by ;
then A10: p . k in the Sorts of () . (() /. k) by ;
q . k = (() . (() /. k)) . (p . k) by A3, A4, A8;
hence q . k in the Sorts of () . (() /. k) by ; :: thesis: verum
end;
A11: now :: thesis: for k being Nat st k in dom p holds
p . k in the Sorts of () . (() /. k)
let k be Nat; :: thesis: ( k in dom p implies p . k in the Sorts of () . (() /. k) )
assume k in dom p ; :: thesis: p . k in the Sorts of () . (() /. k)
then A12: k in dom () by ;
then p . k in the Sorts of () . (() . k) by ;
hence p . k in the Sorts of () . (() /. k) by ; :: thesis: verum
end;
then reconsider x = p as Element of Args ((),()) by ;
A13: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;
then A14: Args ((),()) = (((FreeSort the Sorts of A) #) * the Arity of IIG) . () by MSUALG_1:def 4;
then reconsider pp = p as FinSequence of TS (DTConMSA the Sorts of A) by ;
p in Args ((),()) by ;
then A15: Sym ((), the Sorts of A) ==> roots pp by ;
A16: len q = len () by ;
then reconsider y = q as Element of Args ((),()) by ;
A17: Fix_inp_ext iv is_homomorphism FreeEnv A, FreeEnv A by Def2;
reconsider qq = q as FinSequence of TS (DTConMSA the Sorts of A) by ;
q in Args ((),()) by ;
then A18: Sym ((), the Sorts of A) ==> roots qq by ;
for k being Nat st k in dom p holds
q . k = (() . (() /. k)) . (p . k) by A4;
then A19: y = () # x by MSUALG_3:def 6;
e = (Sym ((), the Sorts of A)) -tree pp by
.= (DenOp ((), the Sorts of A)) . x by
.= ( the Charact of () . ()) . x by
.= (Den ((),())) . x by MSUALG_1:def 6 ;
hence (() . v) . e = (Den ((),())) . q by
.= ((FreeOper the Sorts of A) . ()) . q by
.= (DenOp ((), the Sorts of A)) . q by MSAFREE:def 13
.= (Sym ((), the Sorts of A)) -tree qq by
.= [(), the carrier of IIG] -tree q by MSAFREE:def 9 ;
:: thesis: verum