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