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