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)
consider e being Element of the Sorts of (FreeEnv SCS) . v such that
A1: ( card e = size v,SCS & IGTree v,iv = ((Fix_inp_ext iv) . v) . e ) by Def3;
reconsider igt = IGTree v,iv as Element of the Sorts of (FreeEnv SCS) . v ;
card igt = size v,SCS by A1, Th7;
hence IGTree v,iv = ((Fix_inp_ext iv) . v) . (IGTree v,iv) by Def3; :: thesis: verum