for S being non empty non void ManySortedSign
for A being non-empty finite-yielding MSAlgebra over S
for V being Variables of A
for X being SetWithCompoundTerm of S,V
for G being non empty non void Circuit-like ManySortedSign
for C being non-empty Circuit of G st X,A specifies C holds
for t being Term of S,V st t in Subtrees X holds
ex v being Vertex of G st
for s being State of C holds
( Following (s,(1 + (height (dom t)))) is_stable_at v & ex f being SortMap of X,A,C st
for s9 being State of (X -Circuit A) st s9 = s * f holds
for h being CompatibleValuation of s9 holds (Following (s,(1 + (height (dom t))))) . v = t @ (h,A) ) by Th58, Th60;