let T1, T2 be DecoratedTree; ( dom T1 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
T1 . q = T . (p ^ q) ) & dom T2 = (dom T) | p & ( for q being FinSequence of NAT st q in (dom T) | p holds
T2 . q = T . (p ^ q) ) implies T1 = T2 )
assume that
A1:
dom T1 = (dom T) | p
and
A2:
for q being FinSequence of NAT st q in (dom T) | p holds
T1 . q = T . (p ^ q)
and
A3:
dom T2 = (dom T) | p
and
A4:
for q being FinSequence of NAT st q in (dom T) | p holds
T2 . q = T . (p ^ q)
; T1 = T2
hence
T1 = T2
by A1, A3, Th31; verum