( ( for
p
being
Node
of
T1
holds
T1
.
p
=
T2
.
p
) &
dom
T1
=
dom
T2
implies for
x
being
object
st
x
in
dom
T1
holds
T1
.
x
=
T2
.
x
) ;
hence
(
T1
=
T2
iff (
dom
T1
=
dom
T2
& ( for
p
being
Node
of
T1
holds
T1
.
p
=
T2
.
p
) ) )
by
FUNCT_1:2
;
:: thesis:
verum