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 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ((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 ;

:: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ((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 ;

:: thesis: verum