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 x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let A be non-empty Circuit of IIG; for iv being InputValues of A
for v being Vertex of IIG
for x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let iv be InputValues of A; for v being Vertex of IIG
for x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let v be Vertex of IIG; for x being Element of the Sorts of A . v st v in InputVertices IIG holds
((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
let x be Element of the Sorts of A . v; ( v in InputVertices IIG implies ((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v] )
set e = root-tree [x,v];
assume A1:
v in InputVertices IIG
; ((Fix_inp_ext iv) . v) . (root-tree [x,v]) = root-tree [(iv . v),v]
A2:
root-tree [x,v] in FreeGen (v, the Sorts of A)
by MSAFREE:def 15;
Fix_inp iv c= Fix_inp_ext iv
by Def2;
then A3:
(Fix_inp iv) . v c= (Fix_inp_ext iv) . v
;
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 14;
then reconsider e = root-tree [x,v] as Element of the Sorts of (FreeEnv A) . v by A2;
e in (FreeGen the Sorts of A) . v
by A2, MSAFREE:def 16;
then
e in dom ((Fix_inp iv) . v)
by FUNCT_2:def 1;
hence ((Fix_inp_ext iv) . v) . (root-tree [x,v]) =
((Fix_inp iv) . v) . e
by A3, GRFUNC_1:2
.=
((FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v])) . e
by A1, Def1
.=
root-tree [(iv . v),v]
by A2, FUNCOP_1:7
;
verum