let IIG be non empty non void Circuit-like monotonic ManySortedSign ; 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; 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; 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; ( 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) )
; 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
; e . {} = [(action_at v), the carrier of IIG]
thus
e . {} = [(action_at v), the carrier of IIG]
by A1, TREES_4:def 4; verum