let t1, t2 be DecoratedTree; :: thesis: ( t1 is finite & Subtrees t1 = Subtrees t2 implies t1 = t2 )
assume that
A1: t1 is finite and
A2: Subtrees t1 = Subtrees t2 ; :: thesis: t1 = t2
reconsider t = t1 as finite DecoratedTree by A1;
t1 in Subtrees t2 by A2, Th11;
then consider n being Node of t2 such that
A3: t1 = t2 | n ;
t2 in Subtrees t1 by A2, Th11;
then consider m being Node of t1 such that
A4: t2 = t1 | m ;
dom (t1 | m) = (dom t1) | m by TREES_2:def 10;
then reconsider p = m ^ n as Element of dom t by A4, TREES_1:def 6;
t = t | p by A3, A4, Th3;
then dom t = (dom t) | p by TREES_2:def 10;
then n = {} by Th9;
hence t1 = t2 by A3, Th1; :: thesis: verum