let p be FinSequence of NAT ; :: thesis: for T being DecoratedTree st p in dom T holds
rng (T | p) c= rng T
let T be DecoratedTree; :: thesis: ( p in dom T implies rng (T | p) c= rng T )
assume A1: p in dom T ; :: thesis: rng (T | p) c= rng T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (T | p) or x in rng T )
assume x in rng (T | p) ; :: thesis: x in rng T
then consider y being set such that
A3: y in dom (T | p) and
A4: x = (T | p) . y by FUNCT_1:def 5;
reconsider y = y as Element of dom (T | p) by A3;
A5: dom (T | p) = (dom T) | p by Def11;
then A6: p ^ y in dom T by A1, TREES_1:def 9;
x = T . (p ^ y) by A4, A5, Def11;
hence x in rng T by A6, FUNCT_1:def 5; :: thesis: verum