let IIG be non empty non void Circuit-like monotonic ManySortedSign ; :: thesis: for A being non-empty finite-yielding MSAlgebra over 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 over 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 ( 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]
then A1: ex q being DTree-yielding FinSequence st e = [(action_at v), the carrier of IIG] -tree q by Th12;
take action_at v ; :: thesis: e . {} = [(action_at v), the carrier of IIG]
thus e . {} = [(action_at v), the carrier of IIG] by A1, TREES_4:def 4; :: thesis: verum