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