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 x being set st x in InputVertices S holds
for n being Element of NAT holds (Following s,n) . x = s . x
let A be non-empty Circuit of S; :: thesis: for s being State of A
for x being set st x in InputVertices S holds
for n being Element of NAT holds (Following s,n) . x = s . x
let s be State of A; :: thesis: for x being set st x in InputVertices S holds
for n being Element of NAT holds (Following s,n) . x = s . x
let x be set ; :: thesis: ( x in InputVertices S implies for n being Element of NAT holds (Following s,n) . x = s . x )
assume A1: x in InputVertices S ; :: thesis: for n being Element of NAT holds (Following s,n) . x = s . x
defpred S₁[ Element of NAT ] means (Following s,$1) . x = s . x;

A2: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(Following s,(n + 1)) . x = (Following (Following s,n)) . x by FACIRC_1:12
.= s . x by A1, A3, CIRCUIT2:def 5 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A4: S₁[ 0 ] by FACIRC_1:11;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2); :: thesis: verum