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₁[ Nat] means Following s,(n + $1) = Following (Following s,n),$1;
A1: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A2: Following s,(n + m) = Following (Following s,n),m ; :: thesis: S₁[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;

A3: S₁[ 0 ] by Th11;
thus for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A1); :: thesis: verum