let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s holds args (x -term) = {}
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s holds args (x -term) = {}
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s holds args (x -term) = {}
let x be Element of X . s; :: thesis: args (x -term) = {}
( (x -term) . {} = [x,s] & x -term = [x,s] -tree {} ) by TREES_4:3, TREES_4:20;
hence args (x -term) = {} by ABCMIZ_A:def 10; :: thesis: verum