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