let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for SCS being non-empty Circuit of IIG
for s being State of SCS
for iv being InputValues of SCS
for k being Nat st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let SCS be non-empty Circuit of IIG; :: thesis: for s being State of SCS
for iv being InputValues of SCS
for k being Nat st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let s be State of SCS; :: thesis: for iv being InputValues of SCS
for k being Nat st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let iv be InputValues of SCS; :: thesis: for k being Nat st ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) holds
for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let k be Nat; :: thesis: ( ( for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ) implies for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv) )
assume A1: for v being Vertex of IIG st depth (v,SCS) <= k holds
s . v = IGValue (v,iv) ; :: thesis: for v1 being Vertex of IIG st depth (v1,SCS) <= k + 1 holds
(Following s) . v1 = IGValue (v1,iv)
let v be Vertex of IIG; :: thesis: ( depth (v,SCS) <= k + 1 implies (Following s) . v = IGValue (v,iv) )
assume A2: depth (v,SCS) <= k + 1 ; :: thesis: (Following s) . v = IGValue (v,iv)
v in the carrier of IIG ;
then A3: v in (InputVertices IIG) \/ (InnerVertices IIG) by XBOOLE_1:45;

per cases ( v in InputVertices IIG or v in InnerVertices IIG ) by A3, XBOOLE_0:def 3;

suppose A4: v in InputVertices IIG ; :: thesis: (Following s) . v = IGValue (v,iv)

then A5: depth (v,SCS) = 0 by CIRCUIT1:18;
thus (Following s) . v = s . v by A4, Def5
.= IGValue (v,iv) by A1, A5, NAT_1:2 ; :: thesis: verum

end;

suppose A6: v in InnerVertices IIG ; :: thesis: (Following s) . v = IGValue (v,iv)

set F = Eval SCS;
set X = the Sorts of SCS;
set U1 = FreeEnv SCS;
set o = action_at v;
set taofo = the_arity_of (action_at v);
deffunc H₁( Nat) -> Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. $1) = IGTree (((the_arity_of (action_at v)) /. $1),iv);
consider p being FinSequence such that
A7: len p = len (the_arity_of (action_at v)) and
A8: for k being Nat st k in dom p holds
p . k = H₁(k) from FINSEQ_1:sch 2();
A9: for k being Element of NAT st k in dom p holds
p . k = H₁(k) by A8;

A10: now :: thesis: for k being Nat st k in dom p holds
p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)

let k be Nat; :: thesis: ( k in dom p implies p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) )
assume k in dom p ; :: thesis: p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k)
then p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A8;
hence p . k in the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ; :: thesis: verum

end;

FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 14;
then A11: Den ((action_at v),(FreeEnv SCS)) = (FreeOper the Sorts of SCS) . (action_at v) by MSUALG_1:def 6
.= DenOp ((action_at v), the Sorts of SCS) by MSAFREE:def 13 ;
reconsider ods = (action_at v) depends_on_in s as Function ;
A12: Eval SCS is_homomorphism FreeEnv SCS,SCS by MSAFREE2:def 9;
dom the Arity of IIG = the carrier' of IIG by FUNCT_2:def 1;
then A13: (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) = ( the Sorts of SCS #) . ( the Arity of IIG . (action_at v)) by FUNCT_1:13
.= ( the Sorts of SCS #) . (the_arity_of (action_at v)) by MSUALG_1:def 1
.= product ( the Sorts of SCS * (the_arity_of (action_at v))) by FINSEQ_2:def 5 ;
A14: dom p = dom (the_arity_of (action_at v)) by A7, FINSEQ_3:29;
reconsider p = p as Element of Args ((action_at v),(FreeEnv SCS)) by A7, A10, MSAFREE2:5;
A15: ( FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) & Args ((action_at v),(FreeEnv SCS)) = (( the Sorts of (FreeEnv SCS) #) * the Arity of IIG) . (action_at v) ) by MSAFREE:def 14, MSUALG_1:def 4;
then reconsider p9 = p as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;
Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A15, MSAFREE:10;
then A16: (Den ((action_at v),(FreeEnv SCS))) . p = (Sym ((action_at v), the Sorts of SCS)) -tree p9 by A11, MSAFREE:def 12
.= [(action_at v), the carrier of IIG] -tree p9 by MSAFREE:def 9
.= IGTree (v,iv) by A6, A9, A14, Th9 ;
reconsider Fp = (Eval SCS) # p as Function ;
A17: Args ((action_at v),SCS) = (( the Sorts of SCS #) * the Arity of IIG) . (action_at v) by MSUALG_1:def 4;

now :: thesis: ( dom (the_arity_of (action_at v)) = dom Fp & dom (the_arity_of (action_at v)) = dom ods & ( for x being object st x in dom (the_arity_of (action_at v)) holds
Fp . x = ods . x ) )

( dom the Sorts of SCS = the carrier of IIG & rng (the_arity_of (action_at v)) c= the carrier of IIG ) by FINSEQ_1:def 4, PARTFUN1:def 2;
hence dom (the_arity_of (action_at v)) = dom ( the Sorts of SCS * (the_arity_of (action_at v))) by RELAT_1:27
.= dom Fp by A13, A17, CARD_3:9 ;
:: thesis: ( dom (the_arity_of (action_at v)) = dom ods & ( for x being object st x in dom (the_arity_of (action_at v)) holds
Fp . x = ods . x ) )
( dom s = the carrier of IIG & rng (the_arity_of (action_at v)) c= the carrier of IIG ) by CIRCUIT1:3, FINSEQ_1:def 4;
hence dom (the_arity_of (action_at v)) = dom (s * (the_arity_of (action_at v))) by RELAT_1:27
.= dom ods by CIRCUIT1:def 3 ;
:: thesis: for x being object st x in dom (the_arity_of (action_at v)) holds
Fp . x = ods . x
let x be object ; :: thesis: ( x in dom (the_arity_of (action_at v)) implies Fp . x = ods . x )
reconsider v1 = (the_arity_of (action_at v)) /. x as Element of IIG ;
assume A18: x in dom (the_arity_of (action_at v)) ; :: thesis: Fp . x = ods . x
then reconsider x9 = x as Element of NAT ;
A19: v1 = (the_arity_of (action_at v)) . x9 by A18, PARTFUN1:def 6;
then v1 in rng (the_arity_of (action_at v)) by A18, FUNCT_1:def 3;
then depth (v1,SCS) < k + 1 by A2, A6, CIRCUIT1:19, XXREAL_0:2;
then A20: depth (v1,SCS) <= k by NAT_1:13;
thus Fp . x = ((Eval SCS) . v1) . (p9 . x9) by A14, A18, MSUALG_3:def 6
.= IGValue (v1,iv) by A8, A14, A18
.= s . v1 by A1, A20
.= (s * (the_arity_of (action_at v))) . x by A18, A19, FUNCT_1:13
.= ods . x by CIRCUIT1:def 3 ; :: thesis: verum

end;

then (Eval SCS) # p = (action_at v) depends_on_in s by FUNCT_1:2;
hence (Following s) . v = (Den ((action_at v),SCS)) . ((Eval SCS) # p) by A6, Def5
.= ((Eval SCS) . (the_result_sort_of (action_at v))) . ((Den ((action_at v),(FreeEnv SCS))) . p) by A12, MSUALG_3:def 7
.= IGValue (v,iv) by A6, A16, MSAFREE2:def 7 ;
:: thesis: verum

end;

end;