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 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 ; :: thesis: verum

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 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 ; :: thesis: verum