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 (Following s) & ( for x being object st x in dom iv holds
iv . x = (Following s) . x ) )

dom s = the carrier of IIG by CIRCUIT1:3
.= dom (Following s) by CIRCUIT1:3 ;
hence dom iv c= dom (Following s) by A1, RELAT_1:11; :: thesis: for x being object st x in dom iv holds
iv . x = (Following s) . x
let x be object ; :: thesis: ( x in dom iv implies iv . x = (Following s) . x )
assume A2: x in dom iv ; :: thesis: iv . x = (Following s) . 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 A1, A2, GRFUNC_1:2;
hence iv . x = (Following s) . x by A2, A3, Def5; :: thesis: verum

end;

hence iv c= Following s by GRFUNC_1:2; :: thesis: verum