A1:
( ( for p being Node of T1 holds T1 . p = T2 . p ) & dom T1 = dom T2 implies for x being set st x in dom T1 holds
T1 . x = T2 . x )
;
thus
( T1 = T2 iff ( dom T1 = dom T2 & ( for p being Node of T1 holds T1 . p = T2 . p ) ) )
by A1, FUNCT_1:9; verum