let t be DecoratedTree; :: thesis: for p being Node of t
for k being Element of NAT holds p | k is Node of t
let p be Node of t; :: thesis: for k being Element of NAT holds p | k is Node of t
let k be Element of NAT ; :: thesis: p | k is Node of t
p | k = p | (Seg k) by FINSEQ_1:def 16;
then p | k is_a_prefix_of p by TREES_1:def 1;
hence p | k is Node of t by TREES_1:20; :: thesis: verum