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 x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

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 x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

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 x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v

for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

let x be set ; :: thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] implies ((Fix_inp_ext iv) . v) . e = e )

assume that

A1: v in (InnerVertices IIG) \ (SortsWithConstants IIG) and

A2: e = root-tree [x,v] ; :: thesis: ((Fix_inp_ext iv) . v) . e = e

A3: e . {} = [x,v] by A2, TREES_4:3;

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

then e in (FreeSort the Sorts of A) . v ;

then A6: e in FreeSort ( the Sorts of A,v) by MSAFREE:def 11;

Fix_inp iv c= Fix_inp_ext iv by Def2;

then A7: (Fix_inp iv) . v c= (Fix_inp_ext iv) . v ;

FreeSort ( the Sorts of A,v) = { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st

( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st

( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) } by MSAFREE:def 10;

then ex a being Element of TS (DTConMSA the Sorts of A) st

( a = e & ( ex x being set st

( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st

( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) ) by A6;

then A8: e in FreeGen (v, the Sorts of A) by A4, MSAFREE:def 15;

then e in (FreeGen the Sorts of A) . v by MSAFREE:def 16;

then e in dom ((Fix_inp iv) . v) by FUNCT_2:def 1;

hence ((Fix_inp_ext iv) . v) . e = ((Fix_inp iv) . v) . e by A7, GRFUNC_1:2

.= (id (FreeGen (v, the Sorts of A))) . e by A1, Def1

.= e by A8, FUNCT_1:17 ;

:: 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 x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

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 x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

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 x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v

for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: for x being set st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] holds

((Fix_inp_ext iv) . v) . e = e

let x be set ; :: thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & e = root-tree [x,v] implies ((Fix_inp_ext iv) . v) . e = e )

assume that

A1: v in (InnerVertices IIG) \ (SortsWithConstants IIG) and

A2: e = root-tree [x,v] ; :: thesis: ((Fix_inp_ext iv) . v) . e = e

A3: e . {} = [x,v] by A2, TREES_4:3;

A4: now :: thesis: for o being OperSymbol of IIG holds

( not [o, the carrier of IIG] = e . {} or not the_result_sort_of o = v )

set X = the Sorts of A;( not [o, the carrier of IIG] = e . {} or not the_result_sort_of o = v )

given o being OperSymbol of IIG such that A5:
[o, the carrier of IIG] = e . {}
and

the_result_sort_of o = v ; :: thesis: contradiction

v = the carrier of IIG by A3, A5, XTUPLE_0:1;

hence contradiction by Lm1; :: thesis: verum

end;the_result_sort_of o = v ; :: thesis: contradiction

v = the carrier of IIG by A3, A5, XTUPLE_0:1;

hence contradiction by Lm1; :: thesis: verum

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

then e in (FreeSort the Sorts of A) . v ;

then A6: e in FreeSort ( the Sorts of A,v) by MSAFREE:def 11;

Fix_inp iv c= Fix_inp_ext iv by Def2;

then A7: (Fix_inp iv) . v c= (Fix_inp_ext iv) . v ;

FreeSort ( the Sorts of A,v) = { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st

( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st

( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) } by MSAFREE:def 10;

then ex a being Element of TS (DTConMSA the Sorts of A) st

( a = e & ( ex x being set st

( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st

( [o, the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) ) by A6;

then A8: e in FreeGen (v, the Sorts of A) by A4, MSAFREE:def 15;

then e in (FreeGen the Sorts of A) . v by MSAFREE:def 16;

then e in dom ((Fix_inp iv) . v) by FUNCT_2:def 1;

hence ((Fix_inp_ext iv) . v) . e = ((Fix_inp iv) . v) . e by A7, GRFUNC_1:2

.= (id (FreeGen (v, the Sorts of A))) . e by A1, Def1

.= e by A8, FUNCT_1:17 ;

:: thesis: verum