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