let x, y be set ; :: thesis: for p being DTree-yielding FinSequence st p is V32() holds
for t being DecoratedTree st x in Subtrees t & t in rng p holds
x <> y -tree p
let p be DTree-yielding FinSequence; :: thesis: ( p is V32() implies for t being DecoratedTree st x in Subtrees t & t in rng p holds
x <> y -tree p )
assume A1: p is V32() ; :: thesis: for t being DecoratedTree st x in Subtrees t & t in rng p holds
x <> y -tree p
let t be DecoratedTree; :: thesis: ( x in Subtrees t & t in rng p implies x <> y -tree p )
assume A2: ( x in Subtrees t & t in rng p ) ; :: thesis: x <> y -tree p
reconsider t = t as finite DecoratedTree by A1, A2;
x is Element of Subtrees t by A2;
then reconsider x = x as finite DecoratedTree ;
reconsider p = p as V32() DTree-yielding FinSequence by A1;
consider z being object such that
A3: ( z in dom p & t = p . z ) by A2, FUNCT_1:def 3;
reconsider z = z as Nat by A3;
consider i being Nat such that
A4: z = 1 + i by A3, FINSEQ_3:25, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
z <= len p by A3, FINSEQ_3:25;
then A5: i < len p by A4, NAT_1:13;
A6: dom (y -tree p) = tree (doms p) by TREES_4:10;
A7: len (doms p) = len p by TREES_3:38;
A8: dom t = (doms p) . z by A3, FUNCT_6:22;
consider h being FinSequence of NAT such that
A9: ( h in dom t & len h = height (dom t) ) by TREES_1:def 12;
<*i*> ^ h in dom (y -tree p) by A4, A5, A6, A7, A8, A9, TREES_3:48;
then len (<*i*> ^ h) <= height (dom (y -tree p)) by TREES_1:def 12;
then ( (len <*i*>) + (len h) <= height (dom (y -tree p)) & len <*i*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40;
hence x <> y -tree p by A2, Th6, A9, NAT_1:13; :: thesis: verum