let f1, f2 be Function of (C -Subtrees X),((Subtrees X) *); :: thesis: ( ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f2 . d holds
d = (d . {}) -tree p ) implies f1 = f2 )
assume A9: ( ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees X holds
for p being FinSequence of Subtrees X st p = f2 . d holds
d = (d . {}) -tree p ) ) ; :: thesis: f1 = f2

now :: thesis: for x being object st x in C -Subtrees X holds
f1 . x = f2 . x

let x be object ; :: thesis: ( x in C -Subtrees X implies f1 . x = f2 . x )
assume A10: x in C -Subtrees X ; :: thesis: f1 . x = f2 . x
then reconsider s = x as Element of Subtrees X ;
reconsider p1 = f1 . s, p2 = f2 . s as Element of (Subtrees X) * by A10, FUNCT_2:5;
( s = (s . {}) -tree p1 & s = (s . {}) -tree p2 ) by A9, A10;
hence f1 . x = f2 . x by TREES_4:15; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:12; :: thesis: verum