let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis:
let SCS be non-empty Circuit of IIG; :: thesis:
let v be Vertex of IIG; :: thesis:
let iv be InputValues of SCS; :: thesis:
let p be DTree-yielding FinSequence; :: thesis:
assume that
A1: v in InnerVertices IIG and
A2: dom p = dom (the_arity_of (action_at v)) and
A3: for k being Element of NAT st k in dom p holds
p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) ; :: thesis:
set U1 = FreeEnv SCS;
set o = action_at v;

A4: now :: thesis:

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

end;

len p = len (the_arity_of (action_at v)) by A2, FINSEQ_3:29;
then reconsider p99 = p as Element of Args ((action_at v),(FreeEnv SCS)) by A4, MSAFREE2:5;
set X = the Sorts of SCS;
A5: dom the ResultSort of IIG = the carrier' of IIG by FUNCT_2:def 1;
A6: Result ((action_at v),(FreeEnv SCS)) = ( the Sorts of (FreeEnv SCS) * the ResultSort of IIG) . (action_at v) by MSUALG_1:def 5
.= the Sorts of (FreeEnv SCS) . ( the ResultSort of IIG . (action_at v)) by A5, FUNCT_1:13 ;
A7: ( 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 = p99 as FinSequence of TS (DTConMSA the Sorts of SCS) by MSAFREE:8;
FreeEnv SCS = MSAlgebra(# (FreeSort the Sorts of SCS),(FreeOper the Sorts of SCS) #) by MSAFREE:def 14;
then A8: 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 ;
Sym ((action_at v), the Sorts of SCS) ==> roots p9 by A7, MSAFREE:10;
then A9: (Den ((action_at v),(FreeEnv SCS))) . p = (Sym ((action_at v), the Sorts of SCS)) -tree p9 by A8, MSAFREE:def 12
.= [(action_at v), the carrier of IIG] -tree p9 by MSAFREE:def 9 ;
the ResultSort of IIG . (action_at v) = the_result_sort_of (action_at v) by MSUALG_1:def 2
.= v by A1, MSAFREE2:def 7 ;
then reconsider t = [(action_at v), the carrier of IIG] -tree p as Element of the Sorts of (FreeMSA the Sorts of SCS) . v by A9, A6, FUNCT_2:5;

now :: thesis:

let k be Element of NAT ; :: thesis:
set v1 = (the_arity_of (action_at v)) /. k;
assume k in dom p ; :: thesis:
then A10: p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A3;
then reconsider ek = p . k as Element of the Sorts of (FreeEnv SCS) . ((the_arity_of (action_at v)) /. k) ;
take ek = ek; :: thesis:
thus ek = p . k ; :: thesis:
ex e1 being Element of the Sorts of (FreeMSA the Sorts of SCS) . ((the_arity_of (action_at v)) /. k) st
( card e1 = size (((the_arity_of (action_at v)) /. k),SCS) & ek = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . e1 ) by A10, Def3;
hence card ek = size (((the_arity_of (action_at v)) /. k),SCS) by Th7; :: thesis:

end;

then A11: card t = size (v,SCS) by A1, CIRCUIT1:16;

now :: thesis:

let k be Element of NAT ; :: thesis:
assume k in dom p ; :: thesis:
then p . k = IGTree (((the_arity_of (action_at v)) /. k),iv) by A3;
hence p . k = ((Fix_inp_ext iv) . ((the_arity_of (action_at v)) /. k)) . (p . k) by Th8; :: thesis:

end;

then [(action_at v), the carrier of IIG] -tree p = ((Fix_inp_ext iv) . v) . t by A1, Th4;
hence IGTree (v,iv) = [(action_at v), the carrier of IIG] -tree p by A11, Def3; :: thesis: