let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: e = root-tree [x,v]

thus e = root-tree [x,v] by A1, A4; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: e = root-tree [x,v]

thus e = root-tree [x,v] by A1, A4; :: thesis: verum