let T1, T2 be DecoratedTree; :: thesis: ( dom T1 = dom T2 & ( for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p ) implies T1 = T2 )
assume A1: ( dom T1 = dom T2 & ( for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p ) ) ; :: thesis: T1 = T2

now

let x be set ; :: thesis: ( x in dom T1 implies T1 . x = T2 . x )
assume x in dom T1 ; :: thesis: T1 . x = T2 . x
then reconsider p = x as Element of dom T1 ;
T1 . p = T2 . p by A1;
hence T1 . x = T2 . x ; :: thesis: verum

end;

hence T1 = T2 by A1, FUNCT_1:9; :: thesis: verum