let S be non empty non void ManySortedSign ; :: thesis: for V being V2() ManySortedSet of the carrier of S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is Term of S,V
let V be V2() ManySortedSet of the carrier of S; :: thesis: for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is Term of S,V
let s be SortSymbol of S; :: thesis: for v being Element of V . s holds root-tree [v,s] is Term of S,V
let v be Element of V . s; :: thesis: root-tree [v,s] is Term of S,V
reconsider vs = [v,s] as Terminal of (DTConMSA V) by MSAFREE:7;
root-tree vs in TS (DTConMSA V) ;
hence root-tree [v,s] is Term of S,V ; :: thesis: verum