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 object ; :: 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 object such that
A2: y in dom (T | p) and
A3: x = (T | p) . y by FUNCT_1:def 3;
reconsider y = y as Element of dom (T | p) by A2;
A4: dom (T | p) = (dom T) | p by Def10;
then A5: p ^ y in dom T by A1, TREES_1:def 6;
x = T . (p ^ y) by A3, A4, Def10;
hence x in rng T by A5, FUNCT_1:def 3; :: thesis: verum