let T1, T2 be DecoratedTree; :: thesis: ( 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) ; :: thesis: T1 = T2

now :: thesis: for q being FinSequence of NAT st q in (dom T) | p holds
T1 . q = T2 . q

let q be FinSequence of NAT ; :: thesis: ( q in (dom T) | p implies T1 . q = T2 . q )
assume A5: q in (dom T) | p ; :: thesis: T1 . q = T2 . q
then T1 . q = T . (p ^ q) by A2;
hence T1 . q = T2 . q by A4, A5; :: thesis: verum

end;

hence T1 = T2 by A1, A3, Th31; :: thesis: verum