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 holds IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
let SCS be non-empty Circuit of IIG; :: thesis: for v being Vertex of IIG
for iv being InputValues of SCS holds IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
let v be Vertex of IIG; :: thesis: for iv being InputValues of SCS holds IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
let iv be InputValues of SCS; :: thesis: IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv))
reconsider igt = IGTree (v,iv) as Element of the Sorts of (FreeEnv SCS) . v ;
ex e being Element of the Sorts of (FreeEnv SCS) . v st
( card e = size (v,SCS) & IGTree (v,iv) = ((Fix_inp_ext iv) . v) . e ) by Def3;
then card igt = size (v,SCS) by Th7;
hence IGTree (v,iv) = ((Fix_inp_ext iv) . v) . (IGTree (v,iv)) by Def3; :: thesis: verum