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
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v),the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v),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 (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v),the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v),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 (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v),the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v),the carrier of IIG] -tree q
let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v
for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v),the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v),the carrier of IIG] -tree q
let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: for p, q being DTree-yielding FinSequence st v in InnerVertices IIG & e = [(action_at v),the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) holds
((Fix_inp_ext iv) . v) . e = [(action_at v),the carrier of IIG] -tree q
let p, q be DTree-yielding FinSequence; :: thesis: ( v in InnerVertices IIG & e = [(action_at v),the carrier of IIG] -tree p & dom p = dom q & ( for k being Element of NAT st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ) implies ((Fix_inp_ext iv) . v) . e = [(action_at v),the carrier of IIG] -tree q )
assume that
A1: v in InnerVertices IIG and
A2: e = [(action_at v),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 = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) ; :: thesis: ((Fix_inp_ext iv) . v) . e = [(action_at v),the carrier of IIG] -tree q
A5: for k being Nat st k in dom p holds
q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by A4;
A6: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 16;
set o = action_at v;
A7: the_result_sort_of (action_at v) = v by A1, MSAFREE2:def 7;
then A8: len p = len (the_arity_of (action_at v)) by A2, MSAFREE2:13;

A9: now

let k be Nat; :: thesis: ( k in dom p implies p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) )
assume k in dom p ; :: thesis: p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)
then A10: k in dom (the_arity_of (action_at v)) by A8, FINSEQ_3:31;
then p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A7, MSAFREE2:14;
hence p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A10, PARTFUN1:def 8; :: thesis: verum

end;

then A11: p in Args (action_at v),(FreeEnv A) by A8, MSAFREE2:7;
A12: Args (action_at v),(FreeEnv A) = (((FreeSort the Sorts of A) # ) * the Arity of IIG) . (action_at v) by A6, MSUALG_1:def 9;
A13: len q = len (the_arity_of (action_at v)) by A3, A8, FINSEQ_3:31;

A14: now

let k be Nat; :: thesis: ( k in dom q implies q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) )
assume A15: k in dom q ; :: thesis: q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)
then A16: k in dom (the_arity_of (action_at v)) by A3, A8, FINSEQ_3:31;
A17: q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by A3, A4, A15;
p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A7, A16, MSAFREE2:14;
then p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A16, PARTFUN1:def 8;
hence q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A17, FUNCT_2:7; :: thesis: verum

end;

then A18: q in Args (action_at v),(FreeEnv A) by A13, MSAFREE2:7;
reconsider y = q as Element of Args (action_at v),(FreeEnv A) by A13, A14, MSAFREE2:7;
reconsider x = p as Element of Args (action_at v),(FreeEnv A) by A8, A9, MSAFREE2:7;
A19: y = (Fix_inp_ext iv) # x by A5, MSUALG_3:def 8;
reconsider pp = p as FinSequence of TS (DTConMSA the Sorts of A) by A11, A12, MSAFREE:8;
A20: Sym (action_at v),the Sorts of A ==> roots pp by A11, A12, MSAFREE:10;
A21: e = (Sym (action_at v),the Sorts of A) -tree pp by A2, MSAFREE:def 11
.= (DenOp (action_at v),the Sorts of A) . x by A20, MSAFREE:def 14
.= (the Charact of (FreeEnv A) . (action_at v)) . x by A6, MSAFREE:def 15
.= (Den (action_at v),(FreeEnv A)) . x by MSUALG_1:def 11 ;
reconsider qq = q as FinSequence of TS (DTConMSA the Sorts of A) by A12, A18, MSAFREE:8;
A22: Sym (action_at v),the Sorts of A ==> roots qq by A12, A18, MSAFREE:10;
Fix_inp_ext iv is_homomorphism FreeEnv A, FreeEnv A by Def2;
hence ((Fix_inp_ext iv) . v) . e = (Den (action_at v),(FreeEnv A)) . q by A7, A19, A21, MSUALG_3:def 9
.= ((FreeOper the Sorts of A) . (action_at v)) . q by A6, MSUALG_1:def 11
.= (DenOp (action_at v),the Sorts of A) . q by MSAFREE:def 15
.= (Sym (action_at v),the Sorts of A) -tree qq by A22, MSAFREE:def 14
.= [(action_at v),the carrier of IIG] -tree q by MSAFREE:def 11 ;
:: thesis: verum