let S be non empty non void Circuit-like ManySortedSign ; :: thesis: for A being non-empty Circuit of S
for s being State of A st s is stabilizing holds
for x being set st x in InputVertices S holds
(Result s) . x = s . x
let A be non-empty Circuit of S; :: thesis: for s being State of A st s is stabilizing holds
for x being set st x in InputVertices S holds
(Result s) . x = s . x
let s be State of A; :: thesis: ( s is stabilizing implies for x being set st x in InputVertices S holds
(Result s) . x = s . x )
assume s is stabilizing ; :: thesis: for x being set st x in InputVertices S holds
(Result s) . x = s . x
then Result s = Following (s,(stabilization-time s)) by Th2;
hence for x being set st x in InputVertices S holds
(Result s) . x = s . x by Th1; :: thesis: verum