let IIG be non empty finite non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG
for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat holds iv c= (Computation (s,InpFs)) . k
let SCS be non-empty Circuit of IIG; :: thesis: for InpFs being InputFuncs of SCS st commute InpFs is constant & not InputVertices IIG is empty holds
for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat holds iv c= (Computation (s,InpFs)) . k
let InpFs be InputFuncs of SCS; :: thesis: ( commute InpFs is constant & not InputVertices IIG is empty implies for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat holds iv c= (Computation (s,InpFs)) . k )
assume that
A1: commute InpFs is constant and
A2: not InputVertices IIG is empty ; :: thesis: for s being State of SCS
for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat holds iv c= (Computation (s,InpFs)) . k
A3: dom (commute InpFs) = NAT by A2, PRE_CIRC:5;
let s be State of SCS; :: thesis: for iv being InputValues of SCS st iv = (commute InpFs) . 0 holds
for k being Nat holds iv c= (Computation (s,InpFs)) . k
let iv be InputValues of SCS; :: thesis: ( iv = (commute InpFs) . 0 implies for k being Nat holds iv c= (Computation (s,InpFs)) . k )
assume A4: iv = (commute InpFs) . 0 ; :: thesis: for k being Nat holds iv c= (Computation (s,InpFs)) . k
let k be Nat; :: thesis: iv c= (Computation (s,InpFs)) . k
A5: k in NAT by ORDINAL1:def 12;
IIG is with_input_V by A2;
then A6: k -th_InputValues InpFs = (commute InpFs) . k by CIRCUIT1:def 2
.= iv by A1, A4, A3, FUNCT_1:def 10, A5 ;
set Ck = (Computation (s,InpFs)) . k;
( dom iv = InputVertices IIG & dom (Set-Constants SCS) = SortsWithConstants IIG ) by PARTFUN1:def 2;
then A7: dom iv misses dom (Set-Constants SCS) by MSAFREE2:4;

per cases ( k = 0 or ex n being Nat st k = n + 1 ) by NAT_1:6;

suppose A8: k = 0 ; :: thesis: iv c= (Computation (s,InpFs)) . k

then (Computation (s,InpFs)) . k = InitialComp (s,InpFs) by Def9
.= (s +* (0 -th_InputValues InpFs)) +* (Set-Constants SCS) ;
hence iv c= (Computation (s,InpFs)) . k by A6, A7, A8, FUNCT_4:25, FUNCT_4:124; :: thesis: verum

end;

suppose ex n being Nat st k = n + 1 ; :: thesis: iv c= (Computation (s,InpFs)) . k

then consider n being Nat such that
A9: k = n + 1 ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
reconsider Cn = (Computation (s,InpFs)) . n as State of SCS ;
(Computation (s,InpFs)) . k = Following (Cn,(k -th_InputValues InpFs)) by A9, Def9
.= Following (Cn +* iv) by A6 ;
hence iv c= (Computation (s,InpFs)) . k by Th12, FUNCT_4:25; :: thesis: verum

end;

end;