let tr1, tr2 be finite DecoratedTree of ; :: thesis: ( ( for Tr being finite DecoratedTree of holds
( Tr represents x iff tr1 = Tr ) ) & ( for Tr being finite DecoratedTree of holds
( Tr represents x iff tr2 = Tr ) ) implies tr1 = tr2 )
assume that
A2: for Tr being finite DecoratedTree of holds
( Tr represents x iff tr1 = Tr ) and
A3: for Tr being finite DecoratedTree of holds
( Tr represents x iff tr2 = Tr ) ; :: thesis: tr1 = tr2
tr1 represents x by A2;
hence tr1 = tr2 by A3; :: thesis: verum