( ( for p being Node of T1 holds T1 . p = T2 . p ) & dom T1 =dom T2 implies for x being object st x indom 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 ) ) )
byFUNCT_1:2; :: thesis: verum