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 o being OperSymbol of IIG st e . {} = [o,the carrier of IIG]
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 o being OperSymbol of IIG st e . {} = [o,the carrier of IIG]
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 o being OperSymbol of IIG st e . {} = [o,the carrier of IIG]
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 o being OperSymbol of IIG st e . {} = [o,the carrier of IIG] )
assume A1: ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) & card e = size v,A ) ; :: thesis: ex o being OperSymbol of IIG st e . {} = [o,the carrier of IIG]
consider q being DTree-yielding FinSequence such that
A2: e = [(action_at v),the carrier of IIG] -tree q by A1, Th13;
take action_at v ; :: thesis: e . {} = [(action_at v),the carrier of IIG]
thus e . {} = [(action_at v),the carrier of IIG] by A2, TREES_4:def 4; :: thesis: verum