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

set o = action_at v;

A5: the_result_sort_of (action_at v) = v by A1, MSAFREE2:def 7;

then A6: len p = len (the_arity_of (action_at v)) by A2, MSAFREE2:10;

A13: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;

then A14: Args ((action_at v),(FreeEnv A)) = (((FreeSort the Sorts of A) #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4;

then reconsider pp = p as FinSequence of TS (DTConMSA the Sorts of A) by A6, A11, MSAFREE:8, MSAFREE2:5;

p in Args ((action_at v),(FreeEnv A)) by A6, A11, MSAFREE2:5;

then A15: Sym ((action_at v), the Sorts of A) ==> roots pp by A14, MSAFREE:10;

A16: len q = len (the_arity_of (action_at v)) by A3, A6, FINSEQ_3:29;

then reconsider y = q as Element of Args ((action_at v),(FreeEnv A)) by A7, MSAFREE2:5;

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 A14, A16, A7, MSAFREE:8, MSAFREE2:5;

q in Args ((action_at v),(FreeEnv A)) by A16, A7, MSAFREE2:5;

then A18: Sym ((action_at v), the Sorts of A) ==> roots qq by A14, MSAFREE:10;

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;

then A19: y = (Fix_inp_ext iv) # x by MSUALG_3:def 6;

e = (Sym ((action_at v), the Sorts of A)) -tree pp by A2, MSAFREE:def 9

.= (DenOp ((action_at v), the Sorts of A)) . x by A15, MSAFREE:def 12

.= ( the Charact of (FreeEnv A) . (action_at v)) . x by A13, MSAFREE:def 13

.= (Den ((action_at v),(FreeEnv A))) . x by MSUALG_1:def 6 ;

hence ((Fix_inp_ext iv) . v) . e = (Den ((action_at v),(FreeEnv A))) . q by A5, A19, A17, MSUALG_3:def 7

.= ((FreeOper the Sorts of A) . (action_at v)) . q by A13, MSUALG_1:def 6

.= (DenOp ((action_at v), the Sorts of A)) . q by MSAFREE:def 13

.= (Sym ((action_at v), the Sorts of A)) -tree qq by A18, MSAFREE:def 12

.= [(action_at v), the carrier of IIG] -tree q by MSAFREE:def 9 ;

:: thesis: verum

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

set o = action_at v;

A5: the_result_sort_of (action_at v) = v by A1, MSAFREE2:def 7;

then A6: len p = len (the_arity_of (action_at v)) by A2, MSAFREE2:10;

A7: now :: thesis: for k being Nat st k in dom q holds

q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)

q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)

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 A8: k in dom q ; :: thesis: q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)

then A9: k in dom (the_arity_of (action_at v)) by A3, A6, FINSEQ_3:29;

then p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A5, MSAFREE2:11;

then A10: p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A9, PARTFUN1:def 6;

q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by A3, A4, A8;

hence q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A10, FUNCT_2:5; :: thesis: verum

end;assume A8: k in dom q ; :: thesis: q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)

then A9: k in dom (the_arity_of (action_at v)) by A3, A6, FINSEQ_3:29;

then p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A5, MSAFREE2:11;

then A10: p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A9, PARTFUN1:def 6;

q . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by A3, A4, A8;

hence q . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A10, FUNCT_2:5; :: thesis: verum

A11: now :: thesis: for k being Nat st k in dom p holds

p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)

then reconsider x = p as Element of Args ((action_at v),(FreeEnv A)) by A6, MSAFREE2:5;p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)

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 A12: k in dom (the_arity_of (action_at v)) by A6, FINSEQ_3:29;

then p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A5, MSAFREE2:11;

hence p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A12, PARTFUN1:def 6; :: thesis: verum

end;assume k in dom p ; :: thesis: p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k)

then A12: k in dom (the_arity_of (action_at v)) by A6, FINSEQ_3:29;

then p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) . k) by A2, A5, MSAFREE2:11;

hence p . k in the Sorts of (FreeEnv A) . ((the_arity_of (action_at v)) /. k) by A12, PARTFUN1:def 6; :: thesis: verum

A13: FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 14;

then A14: Args ((action_at v),(FreeEnv A)) = (((FreeSort the Sorts of A) #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4;

then reconsider pp = p as FinSequence of TS (DTConMSA the Sorts of A) by A6, A11, MSAFREE:8, MSAFREE2:5;

p in Args ((action_at v),(FreeEnv A)) by A6, A11, MSAFREE2:5;

then A15: Sym ((action_at v), the Sorts of A) ==> roots pp by A14, MSAFREE:10;

A16: len q = len (the_arity_of (action_at v)) by A3, A6, FINSEQ_3:29;

then reconsider y = q as Element of Args ((action_at v),(FreeEnv A)) by A7, MSAFREE2:5;

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 A14, A16, A7, MSAFREE:8, MSAFREE2:5;

q in Args ((action_at v),(FreeEnv A)) by A16, A7, MSAFREE2:5;

then A18: Sym ((action_at v), the Sorts of A) ==> roots qq by A14, MSAFREE:10;

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;

then A19: y = (Fix_inp_ext iv) # x by MSUALG_3:def 6;

e = (Sym ((action_at v), the Sorts of A)) -tree pp by A2, MSAFREE:def 9

.= (DenOp ((action_at v), the Sorts of A)) . x by A15, MSAFREE:def 12

.= ( the Charact of (FreeEnv A) . (action_at v)) . x by A13, MSAFREE:def 13

.= (Den ((action_at v),(FreeEnv A))) . x by MSUALG_1:def 6 ;

hence ((Fix_inp_ext iv) . v) . e = (Den ((action_at v),(FreeEnv A))) . q by A5, A19, A17, MSUALG_3:def 7

.= ((FreeOper the Sorts of A) . (action_at v)) . q by A13, MSUALG_1:def 6

.= (DenOp ((action_at v), the Sorts of A)) . q by MSAFREE:def 13

.= (Sym ((action_at v), the Sorts of A)) -tree qq by A18, MSAFREE:def 12

.= [(action_at v), the carrier of IIG] -tree q by MSAFREE:def 9 ;

:: thesis: verum