let IIG be non empty non void Circuit-like monotonic ManySortedSign ; 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; 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; 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; 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; 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; ( 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)
; ((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;
then reconsider x = p as Element of Args ((action_at v),(FreeEnv A)) by A6, MSAFREE2:5;
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
;
verum