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
for n being Nat holds Following s,(n + 1) = Following (Following s,n)
let A be non-empty Circuit of S; :: thesis: 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; :: thesis: for n being Nat holds Following s,(n + 1) = Following (Following s,n)
let n be Nat; :: thesis: Following s,(n + 1) = Following (Following s,n)
consider f being Function of NAT ,(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 Def8;
thus Following s,(n + 1) = f . (n + 1) by A2, A3, Def8
.= Following (Following s,n) by A1, A3 ; :: thesis: verum