let D be non empty set ; :: thesis: for T being DecoratedTree of D
for x being set st x in dom T holds
T . x is Element of D
let T be DecoratedTree of D; :: thesis: for x being set st x in dom T holds
T . x is Element of D
let x be set ; :: thesis: ( x in dom T implies T . x is Element of D )
assume A1: x in dom T ; :: thesis: T . x is Element of D
consider y being set such that
A2: y = T . x ;
A3: y in rng T by A1, A2, FUNCT_1:def 5;
rng T c= D by TREES_2:def 9;
hence T . x is Element of D by A2, A3; :: thesis: verum