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

let q be FinSequence of NAT ; :: thesis: ( q in (dom T) | p implies T1 . q = T2 . q )
assume A6: 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, A6; :: thesis: verum

end;

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