let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG

for v being Vertex of IIG

for iv being InputValues of SCS st v in InputVertices IIG holds

IGValue (v,iv) = iv . v

let SCS be non-empty Circuit of IIG; :: thesis: for v being Vertex of IIG

for iv being InputValues of SCS st v in InputVertices IIG holds

IGValue (v,iv) = iv . v

let v be Vertex of IIG; :: thesis: for iv being InputValues of SCS st v in InputVertices IIG holds

IGValue (v,iv) = iv . v

let iv be InputValues of SCS; :: thesis: ( v in InputVertices IIG implies IGValue (v,iv) = iv . v )

set X = the Sorts of SCS;

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

( x in the Sorts of SCS . 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, MSAFREE:def 11;

assume A2: v in InputVertices IIG ; :: thesis: IGValue (v,iv) = iv . v

then A3: iv . v in the Sorts of SCS . v by MSAFREE2:def 5;

then root-tree [(iv . v),v] in FreeGen (v, the Sorts of SCS) by MSAFREE:def 15;

then root-tree [(iv . v),v] in (FreeSort the Sorts of SCS) . v ;

then A4: root-tree [(iv . v),v] in FreeSort ( the Sorts of SCS,v) by MSAFREE:def 11;

consider e being Element of the Sorts of (FreeEnv SCS) . v such that

card e = size (v,SCS) and

A5: IGTree (v,iv) = ((Fix_inp_ext iv) . v) . e by Def3;

( e in the Sorts of (FreeMSA the Sorts of SCS) . v & FreeMSA the Sorts of SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) ) by MSAFREE:def 14;

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

( a = e & ( ex x being set st

( x in the Sorts of SCS . 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 A1;

then A6: e in FreeGen (v, the Sorts of SCS) by A2, MSAFREE:def 15, MSAFREE2:2;

Fix_inp iv c= Fix_inp_ext iv by Def2;

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

A8: (Fix_inp iv) . v = (FreeGen (v, the Sorts of SCS)) --> (root-tree [(iv . v),v]) by A2, Def1;

then e in dom ((Fix_inp iv) . v) by A6;

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

hence IGValue (v,iv) = ((Eval SCS) . v) . (root-tree [(iv . v),v]) by A5, A6, A8, FUNCOP_1:7

.= iv . v by A3, A4, MSAFREE2:def 9 ;

:: thesis: verum

for v being Vertex of IIG

for iv being InputValues of SCS st v in InputVertices IIG holds

IGValue (v,iv) = iv . v

let SCS be non-empty Circuit of IIG; :: thesis: for v being Vertex of IIG

for iv being InputValues of SCS st v in InputVertices IIG holds

IGValue (v,iv) = iv . v

let v be Vertex of IIG; :: thesis: for iv being InputValues of SCS st v in InputVertices IIG holds

IGValue (v,iv) = iv . v

let iv be InputValues of SCS; :: thesis: ( v in InputVertices IIG implies IGValue (v,iv) = iv . v )

set X = the Sorts of SCS;

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

( x in the Sorts of SCS . 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, MSAFREE:def 11;

assume A2: v in InputVertices IIG ; :: thesis: IGValue (v,iv) = iv . v

then A3: iv . v in the Sorts of SCS . v by MSAFREE2:def 5;

then root-tree [(iv . v),v] in FreeGen (v, the Sorts of SCS) by MSAFREE:def 15;

then root-tree [(iv . v),v] in (FreeSort the Sorts of SCS) . v ;

then A4: root-tree [(iv . v),v] in FreeSort ( the Sorts of SCS,v) by MSAFREE:def 11;

consider e being Element of the Sorts of (FreeEnv SCS) . v such that

card e = size (v,SCS) and

A5: IGTree (v,iv) = ((Fix_inp_ext iv) . v) . e by Def3;

( e in the Sorts of (FreeMSA the Sorts of SCS) . v & FreeMSA the Sorts of SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) ) by MSAFREE:def 14;

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

( a = e & ( ex x being set st

( x in the Sorts of SCS . 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 A1;

then A6: e in FreeGen (v, the Sorts of SCS) by A2, MSAFREE:def 15, MSAFREE2:2;

Fix_inp iv c= Fix_inp_ext iv by Def2;

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

A8: (Fix_inp iv) . v = (FreeGen (v, the Sorts of SCS)) --> (root-tree [(iv . v),v]) by A2, Def1;

then e in dom ((Fix_inp iv) . v) by A6;

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

hence IGValue (v,iv) = ((Eval SCS) . v) . (root-tree [(iv . v),v]) by A5, A6, A8, FUNCOP_1:7

.= iv . v by A3, A4, MSAFREE2:def 9 ;

:: thesis: verum