let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra of IIG
for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size v,A holds
ex q being DTree-yielding FinSequence st e = [(action_at v),the carrier of IIG] -tree q
let A be non-empty finite-yielding MSAlgebra of IIG; :: thesis: for v being Vertex of IIG
for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size v,A holds
ex q being DTree-yielding FinSequence st e = [(action_at v),the carrier of IIG] -tree q
let v be Vertex of IIG; :: thesis: for e being Element of the Sorts of (FreeEnv A) . v st v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size v,A holds
ex q being DTree-yielding FinSequence st e = [(action_at v),the carrier of IIG] -tree q
let e be Element of the Sorts of (FreeEnv A) . v; :: thesis: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size v,A implies ex q being DTree-yielding FinSequence st e = [(action_at v),the carrier of IIG] -tree q )
assume that
A1: v in (InnerVertices IIG) \ (SortsWithConstants IIG) and
A2: card e = size v,A ; :: thesis: ex q being DTree-yielding FinSequence st e = [(action_at v),the carrier of IIG] -tree q
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #) by MSAFREE:def 16;
then the Sorts of (FreeEnv A) . v = FreeSort the Sorts of A,v by MSAFREE:def 13;
then e in FreeSort the Sorts of A,v ;
then e in { a where a is Element of TS (DTConMSA the Sorts of A) : ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) } by MSAFREE:def 12;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A3: a = e and
A4: ( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of IIG st
( [o,the carrier of IIG] = a . {} & the_result_sort_of o = v ) ) ;
A5: ( v in InnerVertices IIG & not v in SortsWithConstants IIG ) by A1, XBOOLE_0:def 5;
InputVertices IIG misses InnerVertices IIG by XBOOLE_1:79;
then (InputVertices IIG) /\ (InnerVertices IIG) = {} by XBOOLE_0:def 7;
then not v in InputVertices IIG by A5, XBOOLE_0:def 4;
then not v in (InputVertices IIG) \/ (SortsWithConstants IIG) by A5, XBOOLE_0:def 3;
then A6: card e <> 1 by A2, Th11;
reconsider e' = e as non empty finite set ;
1 <= card e' by NAT_1:14;
then 1 < card e' by A6, XXREAL_0:1;
then consider o being OperSymbol of IIG such that
A7: e . {} = [o,the carrier of IIG] by Th8;
A8: NonTerminals (DTConMSA the Sorts of A) = [:the carrier' of IIG,{the carrier of IIG}:] by MSAFREE:6;
the carrier of IIG in {the carrier of IIG} by TARSKI:def 1;
then reconsider nt = [o,the carrier of IIG] as NonTerminal of (DTConMSA the Sorts of A) by A8, ZFMISC_1:106;
consider ts being FinSequence of TS (DTConMSA the Sorts of A) such that
A9: a = nt -tree ts and
nt ==> roots ts by A3, A7, DTCONSTR:10;
reconsider q = ts as DTree-yielding FinSequence ;
take q ; :: thesis: e = [(action_at v),the carrier of IIG] -tree q
consider x being set such that
A10: ( ( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o' being OperSymbol of IIG st
( [o',the carrier of IIG] = a . {} & the_result_sort_of o' = v ) ) by A4;

now

assume a = root-tree [x,v] ; :: thesis: contradiction
then [o,the carrier of IIG] = [x,v] by A3, A7, TREES_4:3;
then A11: the carrier of IIG = v by ZFMISC_1:33;
for X being set holds not X in X ;
hence contradiction by A11; :: thesis: verum

end;

then consider o' being OperSymbol of IIG such that
A12: [o',the carrier of IIG] = a . {} and
A13: the_result_sort_of o' = v by A10;
A14: ( v in InnerVertices IIG & not v in SortsWithConstants IIG ) by A1, XBOOLE_0:def 5;
o = o' by A3, A7, A12, ZFMISC_1:33
.= action_at v by A13, A14, MSAFREE2:def 7 ;
hence e = [(action_at v),the carrier of IIG] -tree q by A3, A9; :: thesis: verum