let S be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for v being Vertex of S
for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds
ex x being Element of the Sorts of A . v st e = root-tree [x,v]
let A be non-empty MSAlgebra over S; for v being Vertex of S
for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds
ex x being Element of the Sorts of A . v st e = root-tree [x,v]
let v be Vertex of S; for e being Element of the Sorts of (FreeEnv A) . v st v in InputVertices S holds
ex x being Element of the Sorts of A . v st e = root-tree [x,v]
let e be Element of the Sorts of (FreeEnv A) . v; ( v in InputVertices S implies ex x being Element of the Sorts of A . v st e = root-tree [x,v] )
FreeEnv A = MSAlgebra(# (FreeSort the Sorts of A),(FreeOper the Sorts of A) #)
by MSAFREE:def 14;
then
e in (FreeSort the Sorts of A) . v
;
then
e in FreeSort ( the Sorts of A,v)
by MSAFREE:def 11;
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 S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) ) }
by MSAFREE:def 10;
then consider a being Element of TS (DTConMSA the Sorts of A) such that
A1:
a = e
and
A2:
( ex x being set st
( x in the Sorts of A . v & a = root-tree [x,v] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = v ) )
;
assume
v in InputVertices S
; ex x being Element of the Sorts of A . v st e = root-tree [x,v]
then consider x being set such that
A3:
x in the Sorts of A . v
and
A4:
a = root-tree [x,v]
by A2, Th2;
reconsider x = x as Element of the Sorts of A . v by A3;
take
x
; e = root-tree [x,v]
thus
e = root-tree [x,v]
by A1, A4; verum