let G1, G2 be non empty non void Circuit-like ManySortedSign ; :: thesis: for f, g being Function
for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Nat holds Following (s1,n) = (Following (s2,n)) * f
let f, g be Function; :: thesis: for C1 being non-empty Circuit of G1
for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Nat holds Following (s1,n) = (Following (s2,n)) * f
let C1 be non-empty Circuit of G1; :: thesis: for C2 being non-empty Circuit of G2 st f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 holds
for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Nat holds Following (s1,n) = (Following (s2,n)) * f
let C2 be non-empty Circuit of G2; :: thesis: ( f,g form_embedding_of C1,C2 & f preserves_inputs_of G1,G2 implies for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Nat holds Following (s1,n) = (Following (s2,n)) * f )
assume that
A1: f,g form_embedding_of C1,C2 and
A2: f preserves_inputs_of G1,G2 ; :: thesis: for s2 being State of C2
for s1 being State of C1 st s1 = s2 * f holds
for n being Nat holds Following (s1,n) = (Following (s2,n)) * f
let s2 be State of C2; :: thesis: for s1 being State of C1 st s1 = s2 * f holds
for n being Nat holds Following (s1,n) = (Following (s2,n)) * f
let s1 be State of C1; :: thesis: ( s1 = s2 * f implies for n being Nat holds Following (s1,n) = (Following (s2,n)) * f )
assume A3: s1 = s2 * f ; :: thesis: for n being Nat holds Following (s1,n) = (Following (s2,n)) * f
defpred S₁[ Nat] means Following (s1,$1) = (Following (s2,$1)) * f;
Following (s1,0) = s1 by FACIRC_1:11;
then A4: S₁[ 0 ] by A3, FACIRC_1:11;

A5: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then Following (Following (s1,n)) = (Following (Following (s2,n))) * f by A1, A2, Th46;
then Following (s1,(n + 1)) = (Following (Following (s2,n))) * f by FACIRC_1:12
.= (Following (s2,(n + 1))) * f by FACIRC_1:12 ;
hence S₁[n + 1] ; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A5); :: thesis: verum