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, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

let A be non-empty Circuit of S; :: thesis: for s being State of A

for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

let s be State of A; :: thesis: for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

let n be Nat; :: thesis: for m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

defpred S_{1}[ Nat] means Following (s,(n + $1)) = Following ((Following (s,n)),$1);

A1: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]
_{1}[ 0 ]
by Th11;

thus for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A3, A1); :: thesis: verum

for s being State of A

for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

let A be non-empty Circuit of S; :: thesis: for s being State of A

for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

let s be State of A; :: thesis: for n, m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

let n be Nat; :: thesis: for m being Nat holds Following (s,(n + m)) = Following ((Following (s,n)),m)

defpred S

A1: for m being Nat st S

S

proof

A3:
S
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A2: Following (s,(n + m)) = Following ((Following (s,n)),m) ; :: thesis: S_{1}[m + 1]

thus Following (s,(n + (m + 1))) = Following (s,((n + m) + 1))

.= Following (Following (s,(n + m))) by Th12

.= Following ((Following (s,n)),(m + 1)) by A2, Th12 ; :: thesis: verum

end;assume A2: Following (s,(n + m)) = Following ((Following (s,n)),m) ; :: thesis: S

thus Following (s,(n + (m + 1))) = Following (s,((n + m) + 1))

.= Following (Following (s,(n + m))) by Th12

.= Following ((Following (s,n)),(m + 1)) by A2, Th12 ; :: thesis: verum

thus for i being Nat holds S