let f1, f2 be Function of (C -Subtrees t),((Subtrees t) *); :: thesis: ( ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f2 . d holds
d = (d . {}) -tree p ) implies f1 = f2 )
assume A8: ( ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f1 . d holds
d = (d . {}) -tree p ) & ( for d being DecoratedTree st d in C -Subtrees t holds
for p being FinSequence of Subtrees t st p = f2 . d holds
d = (d . {}) -tree p ) ) ; :: thesis: f1 = f2
now :: thesis: for x being object st x in C -Subtrees t holds
f1 . x = f2 . x
let x be object ; :: thesis: ( x in C -Subtrees t implies f1 . x = f2 . x )
assume A9: x in C -Subtrees t ; :: thesis: f1 . x = f2 . x
then reconsider s = x as Element of Subtrees t ;
reconsider p1 = f1 . s, p2 = f2 . s as Element of (Subtrees t) * by A9, FUNCT_2:5;
( s = (s . {}) -tree p1 & s = (s . {}) -tree p2 ) by A8, A9;
hence f1 . x = f2 . x by TREES_4:15; :: thesis: verum
end;
hence f1 = f2 by FUNCT_2:12; :: thesis: verum