( ( 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