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 that
A1: dom T1 = dom T2 and
A2: for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p ; :: thesis: T1 = T2

A3: now

let x be set ; :: thesis: ( x in dom T1 implies T1 . x = T2 . x )
assume A4: x in dom T1 ; :: thesis: T1 . x = T2 . x
reconsider p = x as Element of dom T1 by A4;
A5: T1 . p = T2 . p by A2;
thus T1 . x = T2 . x by A5; :: thesis: verum

end;

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