let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st the_arity_of o = {} holds
height (o -term p) = 0
let o be OperSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for p being Element of Args (o,(Free (S,X))) st the_arity_of o = {} holds
height (o -term p) = 0
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st the_arity_of o = {} holds
height (o -term p) = 0
let p be Element of Args (o,(Free (S,X))); :: thesis: ( the_arity_of o = {} implies height (o -term p) = 0 )
assume the_arity_of o = {} ; :: thesis: height (o -term p) = 0
then dom p = dom {} by MSUALG_3:6;
then p = {} ;
then o -term p = root-tree [o, the carrier of S] by TREES_4:20;
hence height (o -term p) = 0 by TREES_1:42; :: thesis: verum