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

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 ) )

hence
iv c= Following s
by GRFUNC_1:2; :: thesis: verumiv . 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;.= 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