let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS st iv c= s holds
iv c= Following s

let SCS be non-empty Circuit of IIG; :: thesis: for s being State of SCS
for iv being InputValues of SCS st iv c= s holds
iv c= Following s

let s be State of SCS; :: thesis: for iv being InputValues of SCS st iv c= s holds
iv c= Following s

let iv be InputValues of SCS; :: thesis: ( iv c= s implies iv c= Following s )
assume A1: iv c= s ; :: thesis: iv c= Following s
now :: thesis: ( dom iv c= dom () & ( for x being object st x in dom iv holds
iv . x = () . x ) )
dom s = the carrier of IIG by CIRCUIT1:3
.= dom () by CIRCUIT1:3 ;
hence dom iv c= dom () by ; :: thesis: for x being object st x in dom iv holds
iv . x = () . x

let x be object ; :: thesis: ( x in dom iv implies iv . x = () . x )
assume A2: x in dom iv ; :: thesis: iv . x = () . x
A3: dom iv = InputVertices IIG by PARTFUN1:def 2;
then reconsider v = x as Vertex of IIG by A2;
iv . v = s . v by ;
hence iv . x = () . x by A2, A3, Def5; :: thesis: verum
end;
hence iv c= Following s by GRFUNC_1:2; :: thesis: verum