let S be non empty non void Circuit-like ManySortedSign ; for A being non-empty Circuit of S
for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
let A be non-empty Circuit of S; for s being State of A
for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
let s be State of A; for n being Nat holds Following (s,(n + 1)) = Following (Following (s,n))
let n be Nat; Following (s,(n + 1)) = Following (Following (s,n))
consider f being sequence of (product the Sorts of A) such that
A1:
Following (s,n) = f . n
and
A2:
f . 0 = s
and
A3:
for n being Nat holds f . (n + 1) = Following (f . n)
by Def7;
thus Following (s,(n + 1)) =
f . (n + 1)
by A2, A3, Def7
.=
Following (Following (s,n))
by A1, A3
; verum