let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for s being SortSymbol of
for v being Element of V . s holds root-tree [v,s] is Term of S,V
let V be V5() ManySortedSet of ; :: thesis: for s being SortSymbol of
for v being Element of V . s holds root-tree [v,s] is Term of S,V
let s be SortSymbol of ; :: 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