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
set X = the Sorts of A;
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 16;
then e in (FreeSort the Sorts of A) . v ;
then A3: e in FreeSort the Sorts of A,v by MSAFREE:def 13;
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 12;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A4: a = e and
A5: ( 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 A3;
A6: e . {} = [x,v] by A2, TREES_4:3;

now

given o being OperSymbol of IIG such that A7: [o,the carrier of IIG] = e . {} and
the_result_sort_of o = v ; :: thesis: contradiction
v = the carrier of IIG by A6, A7, ZFMISC_1:33;
hence contradiction by Lm1; :: thesis: verum

end;

then consider x' being set such that
A8: x' in the Sorts of A . v and
A9: e = root-tree [x',v] by A4, A5;
A10: e in FreeGen v,the Sorts of A by A8, A9, MSAFREE:def 17;
then e in (FreeGen the Sorts of A) . v by MSAFREE:def 18;
then A11: e in dom ((Fix_inp iv) . v) by FUNCT_2:def 1;
Fix_inp iv c= Fix_inp_ext iv by Def2;
then (Fix_inp iv) . v c= (Fix_inp_ext iv) . v by PBOOLE:def 5;
hence ((Fix_inp_ext iv) . v) . e = ((Fix_inp iv) . v) . e by A11, GRFUNC_1:8
.= (id (FreeGen v,the Sorts of A)) . e by A1, Def1
.= e by A10, FUNCT_1:34 ;
:: thesis: verum