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 ;
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) = (() . 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 ;
Fix_inp iv c= Fix_inp_ext iv by Def2;
then A7: (Fix_inp iv) . v c= () . v ;
A8: (Fix_inp iv) . v = (FreeGen (v, the Sorts of SCS)) --> (root-tree [(iv . v),v]) by ;
then e in dom ((Fix_inp iv) . v) by A6;
then ((Fix_inp iv) . v) . e = (() . v) . e by ;
hence IGValue (v,iv) = ((Eval SCS) . v) . (root-tree [(iv . v),v]) by
.= iv . v by ;
:: thesis: verum